hereby :: thesis: ( ( for X being Subset of L ex a being Element of L st
( a is_<=_than X & ( for b being Element of L st b is_<=_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_<=_than X & ( for b being Element of L st b is_<=_than X holds
b <= p ) )
let X be Subset of L; :: thesis: ex p being Element of L st
( p is_<=_than X & ( for b being Element of L st b is_<=_than X holds
b <= p ) )
set Y = { c where c is Element of L : c is_<=_than X } ;
consider p being Element of L such that
A2: { c where c is Element of L : c is_<=_than X } is_<=_than p and
A3: for r being Element of L st { c where c is Element of L : c is_<=_than X } is_<=_than r holds
p <= r by A1;
take p = p; :: thesis: ( p is_<=_than X & ( for b being Element of L st b is_<=_than X holds
b <= p ) )
thus p is_<=_than X :: thesis: for b being Element of L st b is_<=_than X holds
b <= p

proof

let q be Element of L; :: according to LATTICE3:def 8 :: 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_<=_than X } is_<=_than q

proof

let s be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not s in { c where c is Element of L : c is_<=_than X } or s <= q )
assume s in { c where c is Element of L : c is_<=_than X } ; :: thesis: s <= q
then ex t being Element of L st
( s = t & t is_<=_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_<=_than X implies b <= p )
assume b is_<=_than X ; :: thesis: b <= p
then b in { c where c is Element of L : c is_<=_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_<=_than X & ( for b being Element of L st b is_<=_than X holds
b <= a ) ) ; :: thesis: L is complete
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₂ ) ) )
set Y = { c where c is Element of L : X is_<=_than c } ;
{ c where c is Element of L : X is_<=_than c } c= the carrier of L

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { c where c is Element of L : X is_<=_than c } or x in the carrier of L )
assume x in { c where c is Element of L : X is_<=_than c } ; :: thesis: x in the carrier of L
then ex c being Element of L st
( x = c & X is_<=_than c ) ;
hence x in the carrier of L ; :: thesis: verum

end;

then consider p being Element of L such that
A6: p is_<=_than { c where c is Element of L : X is_<=_than c } and
A7: for r being Element of L st r is_<=_than { c where c is Element of L : X is_<=_than c } holds
r <= p by A5;
take p ; :: thesis: ( X is_<=_than p & ( for b₁ being Element of the carrier of L holds
( not X is_<=_than b₁ or p <= b₁ ) ) )
thus X is_<=_than p :: thesis: for b₁ being Element of the carrier of L holds
( not X is_<=_than b₁ or p <= b₁ )

proof

let q be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not q in X or q <= p )
assume A8: q in X ; :: thesis: q <= p
q is_<=_than { c where c is Element of L : X is_<=_than c }

proof

let s be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not s in { c where c is Element of L : X is_<=_than c } or q <= s )
assume s in { c where c is Element of L : X is_<=_than c } ; :: thesis: q <= s
then ex t being Element of L st
( s = t & X is_<=_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_<=_than r or p <= r )
assume X is_<=_than r ; :: thesis: p <= r
then r in { c where c is Element of L : X is_<=_than c } ;
hence p <= r by A6; :: thesis: verum