consider z being set ;
set A = {z};
reconsider R = id {z} as Relation of {z} ;
reconsider R = R as Order of {z} ;
take IT = RelStr(# {z},R #); :: thesis: ( IT is strict & IT is chain-complete & not IT is empty )
reconsider z = z 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

proof

let x be Element of IT; :: thesis: ( x in L implies x <= z )
assume C1: x in L ; :: thesis: x <= z

per cases ( L = {} or L = {z} ) by ZFMISC_1:39;

suppose L = {} ; :: thesis: x <= z

hence x <= z by C1; :: thesis: verum

end;

suppose L = {z} ; :: thesis: x <= z

thus x <= z by TARSKI:def 1; :: thesis: verum

end;

end;

end;

then B2: L is_<=_than z by LATTICE3:def 9;
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 B2, YELLOW_0:15; :: thesis: verum

end;

hence ( IT is strict & IT is chain-complete & not IT is empty ) by DefchainComplete; :: thesis: verum