begin
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
begin
Lm4:
for X, Y being set
for R being Relation st R is_connected_in X & Y c= X holds
R is_connected_in Y
Lm5:
for X, Y being set
for R being Relation st R well_orders X & Y c= X holds
R well_orders Y
:: Chains.
::