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_{1} being Element of the carrier of L st

( X is_less_than b_{1} & ( for b_{2} being Element of the carrier of L holds

( not X is_less_than b_{2} or b_{1} [= b_{2} ) ) )

defpred S_{1}[ set ] means $1 in X;

set Y = { c where c is Element of L : S_{1}[c] } ;

{ c where c is Element of L : S_{1}[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_{1}[c] } is_less_than p
and

A3: for r being Element of L st { c where c is Element of L : S_{1}[c] } is_less_than r holds

p [= r by A1;

take p ; :: thesis: ( X is_less_than p & ( for b_{1} being Element of the carrier of L holds

( not X is_less_than b_{1} or p [= b_{1} ) ) )

thus X is_less_than p :: thesis: for b_{1} being Element of the carrier of L holds

( not X is_less_than b_{1} or p [= b_{1} )

assume A4: X is_less_than r ; :: thesis: p [= r

_{1}[c] } is_less_than r
;

hence p [= r by A3; :: thesis: verum

( 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

( X is_less_than b

( not X is_less_than b

defpred S

set Y = { c where c is Element of L : S

{ c where c is Element of L : S

then consider p being Element of L such that

A2: { c where c is Element of L : S

A3: for r being Element of L st { c where c is Element of L : S

p [= r by A1;

take p ; :: thesis: ( X is_less_than p & ( for b

( not X is_less_than b

thus X is_less_than p :: thesis: for b

( not X is_less_than b

proof

let r be Element of L; :: thesis: ( not X is_less_than r or p [= r )
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_{1}[c] }
;

hence q [= p by A2; :: thesis: verum

end;assume q in X ; :: thesis: q [= p

then q in { c where c is Element of L : S

hence q [= p by A2; :: thesis: verum

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_{1}[c] } holds

q [= r

then
{ c where c is Element of L : Sq [= r

let q be Element of L; :: thesis: ( q in { c where c is Element of L : S_{1}[c] } implies q [= r )

assume q in { c where c is Element of L : S_{1}[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;assume q in { c where c is Element of L : S

then ex v being Element of L st

( q = v & v in X ) ;

hence q [= r by A4; :: thesis: verum

hence p [= r by A3; :: thesis: verum