reconsider X = X as Subset of L ;

A1: now :: thesis: for Y being finite Subset of X st Y <> {} holds

ex_sup_of Y,L

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;Y c= the carrier of L by XBOOLE_1:1;

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

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

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

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

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

hence
finsups X is directed
by A1, A2, Th51; :: thesis: verum"\/" (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;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