environ
vocabularies HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, RELAT_1, ZFMISC_1, ORDINAL1, CARD_1, XCMPLX_0, NAT_1, VALUED_0, QUANTAL1, FREEALG, SETFAM_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, XTUPLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1;
definitions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, SETFAM_1;
theorems TARSKI, XBOOLE_0, FUNCT_1, ZFMISC_1, RELAT_1, XBOOLE_1, SUBSET_1, XTUPLE_0, XREGULAR;
schemes XBOOLE_0, FUNCT_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ZFMISC_1;
constructors HIDDEN, TARSKI, ENUMSET1, SUBSET_1, FUNCT_1, XTUPLE_0, SETFAM_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities ;
expansions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1;
theorem Th1:
for
X,
Y being
set st
Y in X holds
not
X c= Y
Lm1:
( {} is epsilon-transitive & {} is epsilon-connected )
;
theorem Th21:
for
X being
set holds
not for
x being
set holds
(
x in X iff
x is
Ordinal )