Skip to content

Commit 5940fd4

Browse files
committed
Add recnprss to iset.mm
Copied without change from set.mm.
1 parent 4ef9e9b commit 5940fd4

File tree

1 file changed

+6
-0
lines changed

1 file changed

+6
-0
lines changed

iset.mm

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -136601,6 +136601,12 @@ S C_ ( P ( ball ` D ) T ) ) $=
136601136601
POZQUFR $.
136602136602
$}
136603136603

136604+
$( Both ` RR ` and ` CC ` are subsets of ` CC ` . (Contributed by Mario
136605+
Carneiro, 10-Feb-2015.) $)
136606+
recnprss $p |- ( S e. { RR , CC } -> S C_ CC ) $=
136607+
( cr cc cpr wcel wceq wo wss elpri ax-resscn sseq1 mpbiri eqimss jaoi syl )
136608+
ABCDEABFZACFZGACHZABCIPRQPRBCHJABCKLACMNO $.
136609+
136604136610

136605136611
$(
136606136612
###############################################################################

0 commit comments

Comments
 (0)