let L be non empty Poset; :: thesis: ( L is up-complete & L is with_suprema & L is lower-bounded implies L is complete )

assume A5: ( L is up-complete & L is with_suprema & L is lower-bounded ) ; :: thesis: L is complete

then reconsider K = L as non empty with_suprema lower-bounded Poset ;

let X be set ; :: according to LATTICE3:def 12 :: thesis: ex b_{1} being Element of the carrier of L st

( X is_<=_than b_{1} & ( for b_{2} being Element of the carrier of L holds

( not X is_<=_than b_{2} or b_{1} <= b_{2} ) ) )

reconsider X9 = X /\ the carrier of L as Subset of L by XBOOLE_1:17;

reconsider A = X9 as Subset of K ;

consider x being Element of L such that

A9: fX is_<=_than x and

A10: for y being Element of L st fX is_<=_than y holds

x <= y by A5;

take x ; :: thesis: ( X is_<=_than x & ( for b_{1} being Element of the carrier of L holds

( not X is_<=_than b_{1} or x <= b_{1} ) ) )

X9 is_<=_than x by A6, A7, A8, A9, Th52;

hence X is_<=_than x by YELLOW_0:5; :: thesis: for b_{1} being Element of the carrier of L holds

( not X is_<=_than b_{1} or x <= b_{1} )

let y be Element of L; :: thesis: ( not X is_<=_than y or x <= y )

assume y is_>=_than X ; :: thesis: x <= y

then y is_>=_than X9 by YELLOW_0:5;

then y is_>=_than fX by A6, A7, A8, Th52;

hence x <= y by A10; :: thesis: verum

assume A5: ( L is up-complete & L is with_suprema & L is lower-bounded ) ; :: thesis: L is complete

then reconsider K = L as non empty with_suprema lower-bounded Poset ;

let X be set ; :: according to LATTICE3:def 12 :: thesis: ex b

( X is_<=_than b

( not X is_<=_than b

reconsider X9 = X /\ the carrier of L as Subset of L by XBOOLE_1:17;

reconsider A = X9 as Subset of K ;

A6: now :: thesis: for Y being finite Subset of X9 st Y <> {} holds

ex_sup_of Y,L

ex_sup_of Y,L

let Y be finite Subset of X9; :: thesis: ( Y <> {} implies ex_sup_of Y,L )

Y c= the carrier of L by XBOOLE_1:1;

hence ( Y <> {} implies ex_sup_of Y,L ) by A5, YELLOW_0:54; :: thesis: verum

end;Y c= the carrier of L by XBOOLE_1:1;

hence ( Y <> {} implies ex_sup_of Y,L ) by A5, YELLOW_0:54; :: thesis: verum

A7: now :: thesis: for x being Element of L st x in finsups X9 holds

ex Y being finite Subset of X9 st

( ex_sup_of Y,L & x = "\/" (Y,L) )

ex Y being finite Subset of X9 st

( ex_sup_of Y,L & x = "\/" (Y,L) )

let x be Element of L; :: thesis: ( x in finsups X9 implies ex Y being finite Subset of X9 st

( ex_sup_of Y,L & x = "\/" (Y,L) ) )

assume x in finsups X9 ; :: thesis: ex Y being finite Subset of X9 st

( ex_sup_of Y,L & x = "\/" (Y,L) )

then ex Y being finite Subset of X9 st

( x = "\/" (Y,L) & ex_sup_of Y,L ) ;

hence ex Y being finite Subset of X9 st

( ex_sup_of Y,L & x = "\/" (Y,L) ) ; :: thesis: verum

end;( ex_sup_of Y,L & x = "\/" (Y,L) ) )

assume x in finsups X9 ; :: thesis: ex Y being finite Subset of X9 st

( ex_sup_of Y,L & x = "\/" (Y,L) )

then ex Y being finite Subset of X9 st

( x = "\/" (Y,L) & ex_sup_of Y,L ) ;

hence ex Y being finite Subset of X9 st

( ex_sup_of Y,L & x = "\/" (Y,L) ) ; :: thesis: verum

A8: now :: thesis: for Y being finite Subset of X9 st Y <> {} holds

"\/" (Y,L) in finsups X9

reconsider fX = finsups A as non empty directed Subset of L ;"\/" (Y,L) in finsups X9

let Y be finite Subset of X9; :: thesis: ( Y <> {} implies "\/" (Y,L) in finsups X9 )

reconsider Z = Y as Subset of L by XBOOLE_1:1;

assume Y <> {} ; :: thesis: "\/" (Y,L) in finsups X9

then ex_sup_of Z,L by A5, YELLOW_0:54;

hence "\/" (Y,L) in finsups X9 ; :: thesis: verum

end;reconsider Z = Y as Subset of L by XBOOLE_1:1;

assume Y <> {} ; :: thesis: "\/" (Y,L) in finsups X9

then ex_sup_of Z,L by A5, YELLOW_0:54;

hence "\/" (Y,L) in finsups X9 ; :: thesis: verum

consider x being Element of L such that

A9: fX is_<=_than x and

A10: for y being Element of L st fX is_<=_than y holds

x <= y by A5;

take x ; :: thesis: ( X is_<=_than x & ( for b

( not X is_<=_than b

X9 is_<=_than x by A6, A7, A8, A9, Th52;

hence X is_<=_than x by YELLOW_0:5; :: thesis: for b

( not X is_<=_than b

let y be Element of L; :: thesis: ( not X is_<=_than y or x <= y )

assume y is_>=_than X ; :: thesis: x <= y

then y is_>=_than X9 by YELLOW_0:5;

then y is_>=_than fX by A6, A7, A8, Th52;

hence x <= y by A10; :: thesis: verum