hereby :: thesis: ( ( for X being Subset of L ex a being Element of L st
( a is_less_than X & ( for b being Element of L st b is_less_than X holds
b [= a ) ) ) implies L is complete )
assume A1: L is complete ; :: thesis: for X being Subset of L ex p being Element of L st
( p is_less_than X & ( for b being Element of L st b is_less_than X holds
b [= p ) )

let X be Subset of L; :: thesis: ex p being Element of L st
( p is_less_than X & ( for b being Element of L st b is_less_than X holds
b [= p ) )

set Y = { c where c is Element of L : c is_less_than X } ;
consider p being Element of L such that
A2: { c where c is Element of L : c is_less_than X } is_less_than p and
A3: for r being Element of L st { c where c is Element of L : c is_less_than X } is_less_than r holds
p [= r by A1;
take p = p; :: thesis: ( p is_less_than X & ( for b being Element of L st b is_less_than X holds
b [= p ) )

thus p is_less_than X :: thesis: for b being Element of L st b is_less_than X holds
b [= p
proof
let q be Element of L; :: according to LATTICE3:def 16 :: thesis: ( not q in X or p [= q )
assume A4: q in X ; :: thesis: p [= q
{ c where c is Element of L : c is_less_than X } is_less_than q
proof
let s be Element of L; :: according to LATTICE3:def 17 :: thesis: ( not s in { c where c is Element of L : c is_less_than X } or s [= q )
assume s in { c where c is Element of L : c is_less_than X } ; :: thesis: s [= q
then ex t being Element of L st
( s = t & t is_less_than X ) ;
hence s [= q by A4; :: thesis: verum
end;
hence p [= q by A3; :: thesis: verum
end;
let b be Element of L; :: thesis: ( b is_less_than X implies b [= p )
assume b is_less_than X ; :: thesis: b [= p
then b in { c where c is Element of L : c is_less_than X } ;
hence b [= p by A2; :: thesis: verum
end;
assume A5: for X being Subset of L ex a being Element of L st
( a is_less_than X & ( for b being Element of L st b is_less_than X holds
b [= a ) ) ; :: 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[ Element of L] means X is_less_than \$1;
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
A6: p is_less_than { c where c is Element of L : S1[c] } and
A7: for r being Element of L st r is_less_than { c where c is Element of L : S1[c] } holds
r [= p by A5;
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 A8: q in X ; :: thesis: q [= p
q is_less_than { c where c is Element of L : S1[c] }
proof
let s be Element of L; :: according to LATTICE3:def 16 :: thesis: ( not s in { c where c is Element of L : S1[c] } or q [= s )
assume s in { c where c is Element of L : S1[c] } ; :: thesis: q [= s
then ex t being Element of L st
( s = t & X is_less_than t ) ;
hence q [= s by A8; :: thesis: verum
end;
hence q [= p by A7; :: thesis: verum
end;
let r be Element of L; :: thesis: ( not X is_less_than r or p [= r )
assume X is_less_than r ; :: thesis: p [= r
then r in { c where c is Element of L : S1[c] } ;
hence p [= r by A6; :: thesis: verum