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 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₁[ Element of L] means X is_less_than $1;
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
A6: p is_less_than { c where c is Element of L : S₁[c] } and
A7: for r being Element of L st r is_less_than { c where c is Element of L : S₁[c] } holds
r [= p by A5;
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 A8: q in X ; :: thesis: q [= p
q is_less_than { c where c is Element of L : S₁[c] }

proof

let s be Element of L; :: according to LATTICE3:def 16 :: thesis: ( not s in { c where c is Element of L : S₁[c] } or q [= s )
assume s in { c where c is Element of L : S₁[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 : S₁[c] } ;
hence p [= r by A6; :: thesis: verum