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 b1 being Element of the carrier of L st
( X is_less_than b1 & ( for b2 being Element of the carrier of L holds
( not X is_less_than b2 or b1 [= b2 ) ) )

defpred S1[ set ] means \$1 in X;
set Y = { c where c is Element of L : S1[c] } ;
{ c where c is Element of L : S1[c] } is Subset of L from then consider p being Element of L such that
A2: { c where c is Element of L : S1[c] } is_less_than p and
A3: for r being Element of L st { c where c is Element of L : S1[c] } is_less_than r holds
p [= r by A1;
take p ; :: thesis: ( X is_less_than p & ( for b1 being Element of the carrier of L holds
( not X is_less_than b1 or p [= b1 ) ) )

thus X is_less_than p :: thesis: for b1 being Element of the carrier of L holds
( not X is_less_than b1 or p [= b1 )
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 : S1[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 : S1[c] } holds
q [= r
let q be Element of L; :: thesis: ( q in { c where c is Element of L : S1[c] } implies q [= r )
assume q in { c where c is Element of L : S1[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 : S1[c] } is_less_than r ;
hence p [= r by A3; :: thesis: verum