Skip to content

Commit 7e1d87f

Browse files
committed
Add nelss to iset.mm
Copied without change from set.mm.
1 parent 089644c commit 7e1d87f

File tree

1 file changed

+5
-0
lines changed

1 file changed

+5
-0
lines changed

iset.mm

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27453,6 +27453,11 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use
2745327453
IAJBCKPQALABCMN $.
2745427454
$}
2745527455

27456+
$( Demonstrate by witnesses that two classes lack a subclass relation.
27457+
(Contributed by Stefan O'Rear, 5-Feb-2015.) $)
27458+
nelss $p |- ( ( A e. B /\ -. A e. C ) -> -. B C_ C ) $=
27459+
( wcel wss ssel com12 con3dimp ) ABDZBCEZACDZJIKBCAFGH $.
27460+
2745627461
${
2745727462
$d x A $. $d x B $.
2745827463
$( Quantification restricted to a subclass. (Contributed by NM,

0 commit comments

Comments
 (0)