let L be non empty RelStr ; :: thesis: ( ( for X being set holds ex_sup_of X,L ) implies L is complete )
assume A1: for X being set holds ex_sup_of X,L ; :: thesis: L is complete
L is complete

proof

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 a = "\/" (X,L); :: thesis: ( X is_<=_than a & ( for b₁ being Element of the carrier of L holds
( not X is_<=_than b₁ or a <= b₁ ) ) )
A2: ex_sup_of X,L by A1;
hence X is_<=_than a by YELLOW_0:def 9; :: thesis: for b₁ being Element of the carrier of L holds
( not X is_<=_than b₁ or a <= b₁ )
thus for b₁ being Element of the carrier of L holds
( not X is_<=_than b₁ or a <= b₁ ) by A2, YELLOW_0:def 9; :: thesis: verum

end;

hence L is complete ; :: thesis: verum