let L be with_suprema Poset; :: thesis: for X being Subset of L st ( ex_sup_of X,L or L is complete ) holds
sup X = sup (finsups X)
let X be Subset of L; :: thesis: ( ( ex_sup_of X,L or L is complete ) implies sup X = sup (finsups X) )
assume ( ex_sup_of X,L or L is complete ) ; :: thesis: sup X = sup (finsups X)
then A1: ex_sup_of X,L by YELLOW_0:17;

A2: now :: thesis: for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L

let Y be finite Subset of X; :: 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 YELLOW_0:54; :: thesis: verum

end;

A3: now :: thesis: for x being Element of L st x in finsups X holds
ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) )

let x be Element of L; :: thesis: ( x in finsups X implies ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) ) )
assume x in finsups X ; :: thesis: ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) )
then ex Y being finite Subset of X st
( x = "\/" (Y,L) & ex_sup_of Y,L ) ;
hence ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ; :: thesis: verum

end;

now :: thesis: for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in finsups X

let Y be finite Subset of X; :: thesis: ( Y <> {} implies "\/" (Y,L) in finsups X )
reconsider Z = Y as Subset of L by XBOOLE_1:1;
assume Y <> {} ; :: thesis: "\/" (Y,L) in finsups X
then ex_sup_of Z,L by YELLOW_0:54;
hence "\/" (Y,L) in finsups X ; :: thesis: verum

end;

hence sup X = sup (finsups X) by A1, A2, A3, Th54; :: thesis: verum