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
for x being Element of L holds
( x is_>=_than X iff x is_>=_than F )
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 for x being Element of L holds
( x is_>=_than X iff x is_>=_than F ) )
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: for x being Element of L holds
( x is_>=_than X iff x is_>=_than F )
let x be Element of L; :: thesis: ( x is_>=_than X iff x is_>=_than F )
thus ( x is_>=_than X implies x is_>=_than F ) :: thesis: ( x is_>=_than F implies x is_>=_than X )

proof

assume A4: x is_>=_than X ; :: thesis: x is_>=_than F
let y be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not y in F or y <= x )
assume y in F ; :: thesis: y <= x
then consider Y being finite Subset of X such that
A5: ex_sup_of Y,L and
A6: y = "\/" (Y,L) by A2;
x is_>=_than Y by A4;
hence y <= x by A5, A6, YELLOW_0:def 9; :: thesis: verum

end;

assume A7: x is_>=_than F ; :: thesis: x is_>=_than X
let y be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not y in X or y <= x )
assume y in X ; :: thesis: y <= x
then A8: {y} c= X by ZFMISC_1:31;
then A9: sup {y} in F by A3;
ex_sup_of {y},L by A1, A8;
then A10: {y} is_<=_than sup {y} by YELLOW_0:def 9;
A11: sup {y} <= x by A7, A9;
y <= sup {y} by A10, YELLOW_0:7;
hence y <= x by A11, ORDERS_2:3; :: thesis: verum