set z = the set ;
set A = { the set };
reconsider R = id { the set } as Relation of { the set } ;
reconsider R = R as Order of { the set } ;
take IT = RelStr(# { the set },R #); :: thesis: ( IT is strict & IT is chain-complete & not IT is empty )
reconsider z = the set as Element of IT by TARSKI:def 1;
for L being Chain of IT st not L is empty holds
ex_sup_of L,IT
proof
let L be Chain of IT; :: thesis: ( not L is empty implies ex_sup_of L,IT )
assume not L is empty ; :: thesis: ex_sup_of L,IT
for x being Element of IT st x in L holds
x <= z by TARSKI:def 1;
then A1: L is_<=_than z ;
for y being Element of IT st L is_<=_than y holds
z <= y by TARSKI:def 1;
hence ex_sup_of L,IT by A1, YELLOW_0:15; :: thesis: verum
end;
hence ( IT is strict & IT is chain-complete & not IT is empty ) ; :: thesis: verum