let L be non empty RelStr ; :: thesis: ( ( for X being Subset of L holds ex_sup_of X,L ) implies L is complete )
assume A1: for X being Subset of L holds ex_sup_of X,L ; :: thesis: L is complete
let X be set ; :: according to LATTICE3:def 12 :: thesis: ex b₁ being Element of the carrier of L st
( X is_<=_than b₁ & ( for b₂ being Element of the carrier of L holds
( not X is_<=_than b₂ or b₁ <= b₂ ) ) )
take "\/" (X,L) ; :: thesis: ( X is_<=_than "\/" (X,L) & ( for b₁ being Element of the carrier of L holds
( not X is_<=_than b₁ or "\/" (X,L) <= b₁ ) ) )
reconsider Y = X /\ the carrier of L as Subset of L by XBOOLE_1:17;
ex_sup_of Y,L by A1;
then ex_sup_of X,L by Th50;
hence ( X is_<=_than "\/" (X,L) & ( for b₁ being Element of the carrier of L holds
( not X is_<=_than b₁ or "\/" (X,L) <= b₁ ) ) ) by Def9; :: thesis: verum