let L be non empty reflexive transitive RelStr ; :: thesis: for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" Y,L ) ) & ( for Y being finite Subset of X st Y <> {} holds
"\/" Y,L in F ) holds
( ex_sup_of X,L iff ex_sup_of F,L )
let X, F be Subset of L; :: thesis: ( ( for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" Y,L ) ) & ( for Y being finite Subset of X st Y <> {} holds
"\/" Y,L in F ) implies ( ex_sup_of X,L iff ex_sup_of F,L ) )
assume that
A1: for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L and
A2: for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" Y,L ) and
A3: for Y being finite Subset of X st Y <> {} holds
"\/" Y,L in F ; :: thesis: ( ex_sup_of X,L iff ex_sup_of F,L )
for x being Element of L holds
( x is_>=_than X iff x is_>=_than F ) by A1, A2, A3, Th52;
hence ( ex_sup_of X,L iff ex_sup_of F,L ) by YELLOW_0:46; :: thesis: verum