environ
vocabularies HIDDEN, ORDINAL1, CARD_1, SUBSET_1, FUNCT_1, RELAT_1, FUNCOP_1, XBOOLE_0, ZFMISC_1, TARSKI, FUNCT_2, MCART_1, FINSET_1, NAT_1, WELLORD1, WELLORD2, RELAT_2, SETFAM_1, PARTFUN1, FUNCT_4, CARD_3, PBOOLE, NAGATA_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, CARD_1, RELAT_1, RELAT_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, SETFAM_1, ORDINAL1, WELLORD1, MCART_1, WELLORD2, FUNCOP_1, FUNCT_4, FINSET_1, FINSUB_1, PBOOLE;
definitions TARSKI, FUNCT_1, RELAT_2, WELLORD1, WELLORD2, XBOOLE_0, RELAT_1, ORDINAL1, PARTFUN1;
theorems TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, MCART_1, ORDINAL1, RELAT_1, WELLORD1, WELLORD2, CARD_1, FUNCOP_1, FUNCT_5, GRFUNC_1, XBOOLE_0, XBOOLE_1, SETFAM_1, FUNCT_4, PARTFUN1, RELSET_1, SUBSET_1, FINSET_1, XTUPLE_0;
schemes FUNCT_1, PARTFUN1, ORDINAL1, FUNCT_5, RELAT_1, XBOOLE_0, CLASSES1, XFAMILY;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FUNCT_4, FINSET_1, CARD_1, PBOOLE, RELSET_1, XTUPLE_0;
constructors HIDDEN, SETFAM_1, RELAT_2, WELLORD1, PARTFUN1, WELLORD2, FUNCOP_1, FUNCT_4, CLASSES1, ORDINAL2, ORDINAL3, FINSET_1, CARD_1, FINSUB_1, RELSET_1, FUNCT_1, PBOOLE, XTUPLE_0;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET;
equalities XBOOLE_0, FUNCOP_1, RELAT_1, ORDINAL1;
expansions TARSKI, FUNCT_1, RELAT_2, WELLORD1, WELLORD2, XBOOLE_0, RELAT_1, ORDINAL1, PARTFUN1;
defpred S1[ object ] means $1 is Function;
Lm1:
for x being object
for R being Relation st x in field R holds
ex y being object st
( [x,y] in R or [y,x] in R )
Lm2:
for X being functional with_common_domain set
for f being Function st f in X holds
dom f = DOM X
Lm3:
for X, Y being set st Y c= X & X is countable holds
Y is countable
;
Lm4:
for R being Relation st field R is finite holds
R is finite