thus ( L is complete implies for X being Subset of L ex a being Element of L st
( X is_less_than a & ( for b being Element of L st X is_less_than b holds
a [= b ) ) ) ; :: thesis: ( ( for X being Subset of L ex a being Element of L st
( X is_less_than a & ( for b being Element of L st X is_less_than b holds
a [= b ) ) ) implies L is complete )
assume A1: for X being Subset of L ex a being Element of L st
( X is_less_than a & ( for b being Element of L st X is_less_than b holds
a [= b ) ) ; :: thesis: L is complete
let X be set ; :: according to LATTICE3:def 18 :: thesis: ex b₁ being Element of the carrier of L st
( X is_less_than b₁ & ( for b₂ being Element of the carrier of L holds
( not X is_less_than b₂ or b₁ [= b₂ ) ) )
defpred S₁[ set ] means $1 in X;
set Y = { c where c is Element of L : S₁[c] } ;
{ c where c is Element of L : S₁[c] } is Subset of L from DOMAIN_1:sch 7();
then consider p being Element of L such that
A2: { c where c is Element of L : S₁[c] } is_less_than p and
A3: for r being Element of L st { c where c is Element of L : S₁[c] } is_less_than r holds
p [= r by A1;
take p ; :: thesis: ( X is_less_than p & ( for b₁ being Element of the carrier of L holds
( not X is_less_than b₁ or p [= b₁ ) ) )
thus X is_less_than p :: thesis: for b₁ being Element of the carrier of L holds
( not X is_less_than b₁ or p [= b₁ )

proof

let q be Element of L; :: according to LATTICE3:def 17 :: thesis: ( not q in X or q [= p )
assume q in X ; :: thesis: q [= p
then q in { c where c is Element of L : S₁[c] } ;
hence q [= p by A2; :: thesis: verum

end;

let r be Element of L; :: thesis: ( not X is_less_than r or p [= r )
assume A4: X is_less_than r ; :: thesis: p [= r

now :: thesis: for q being Element of L st q in { c where c is Element of L : S₁[c] } holds
q [= r

let q be Element of L; :: thesis: ( q in { c where c is Element of L : S₁[c] } implies q [= r )
assume q in { c where c is Element of L : S₁[c] } ; :: thesis: q [= r
then ex v being Element of L st
( q = v & v in X ) ;
hence q [= r by A4; :: thesis: verum

end;

then { c where c is Element of L : S₁[c] } is_less_than r ;
hence p [= r by A3; :: thesis: verum