environ
vocabularies HIDDEN, STRUCT_0, RELAT_1, XBOOLE_0, PARTFUN1, RELAT_2, ORDERS_1, SUBSET_1, XXREAL_0, ARYTM_3, TREES_2, TARSKI, WELLORD1, FUNCT_1, ZFMISC_1, ORDERS_2, CARD_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1, RELSET_1, PARTFUN1, CARD_1, WELLORD1, DOMAIN_1, STRUCT_0, ORDERS_1;
definitions RELAT_2, TARSKI, WELLORD1, STRUCT_0, XBOOLE_0, ORDERS_1;
theorems RELAT_1, RELAT_2, TARSKI, WELLORD1, ZFMISC_1, XBOOLE_0, XBOOLE_1, PARTFUN1, ORDERS_1, XTUPLE_0;
schemes XFAMILY;
registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, PARTFUN1, CARD_1, RELAT_2;
constructors HIDDEN, RELAT_2, WELLORD1, PARTFUN1, DOMAIN_1, ORDERS_1, PRE_TOPC, RELSET_1, SETFAM_1;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS;
equalities RELAT_1, WELLORD1, STRUCT_0, ORDERS_1;
expansions RELAT_2, TARSKI, WELLORD1, XBOOLE_0, ORDERS_1;
Lm1:
for x being set
for A being non empty Poset
for S being Subset of A st x in S holds
x is Element of A
;
Lm2:
for A being non empty Poset
for f being Choice_Function of (BOOL the carrier of A) holds union (Chains f) is Subset of A
Lm3:
for A being non empty Poset
for f being Choice_Function of (BOOL the carrier of A) holds union (Chains f) is Chain of A
Lm4:
for X, Y being set
for R being Relation st R well_orders X & Y c= X holds
R well_orders Y
:: Chains.
::