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 b1 being Element of the carrier of L st
( X is_<=_than b1 & ( for b2 being Element of the carrier of L holds
( not X is_<=_than b2 or b1 <= b2 ) ) )
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
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;
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) )
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;
A8: now :: thesis: for Y being finite Subset of X9 st Y <> {} holds
"\/" (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 fX = finsups A as non empty directed Subset of L ;
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 b1 being Element of the carrier of L holds
( not X is_<=_than b1 or x <= b1 ) ) )
X9 is_<=_than x by A6, A7, A8, A9, Th52;
hence X is_<=_than x by YELLOW_0:5; :: thesis: for b1 being Element of the carrier of L holds
( not X is_<=_than b1 or x <= b1 )
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