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 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 ) ) ) 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

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;( 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 b be Element of L; :: thesis: ( b is_less_than X implies b [= p )
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

end;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

hence
p [= q
by A3; :: thesis: verum
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;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

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

( 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

( 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

A6: p is_less_than { c where c is Element of L : S

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

r [= p by A5;

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 A8: q in X ; :: thesis: q [= p

q is_less_than { c where c is Element of L : S_{1}[c] }

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

q is_less_than { c where c is Element of L : S

proof

hence
q [= p
by A7; :: thesis: verum
let s be Element of L; :: according to LATTICE3:def 16 :: thesis: ( not s in { c where c is Element of L : S_{1}[c] } or q [= s )

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

then ex t being Element of L st

( s = t & X is_less_than t ) ;

hence q [= s by A8; :: thesis: verum

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

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

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