environ
vocabularies HIDDEN, RELAT_1, ORDINAL1, TARSKI, RELAT_2, WELLORD1, XBOOLE_0, SUBSET_1, ZFMISC_1, FUNCT_1, WELLORD2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, MCART_1, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1, WELLORD1, ORDINAL1;
definitions TARSKI, XBOOLE_0, FUNCT_1, RELAT_1, RELAT_2, WELLORD1;
theorems TARSKI, FUNCT_1, RELAT_1, RELAT_2, ZFMISC_1, WELLORD1, ORDINAL1, XBOOLE_0, XTUPLE_0;
schemes FUNCT_1, RELAT_1, ORDINAL1, XBOOLE_0;
registrations RELAT_1, FUNCT_1, ORDINAL1, WELLORD1;
constructors HIDDEN, RELAT_2, ORDINAL1, WELLORD1, MCART_1, XTUPLE_0;
requirements HIDDEN, SUBSET, BOOLE;
equalities TARSKI, XBOOLE_0, RELAT_1, WELLORD1;
expansions TARSKI, XBOOLE_0, FUNCT_1, RELAT_2, WELLORD1;
Lm1:
for X being set
for R being Relation st R is well-ordering & X, field R are_equipotent holds
ex R being Relation st R well_orders X