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

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

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