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_inf_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_inf_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_inf_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_inf_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_inf_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_inf_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 8 :: thesis: ( not y in F or x <= y )
assume y in F ; :: thesis: x <= y
then consider Y being finite Subset of X such that
A5: ( ex_inf_of Y,L & y = "/\" Y,L ) by A2;
x is_<=_than Y by A4, YELLOW_0:9;
hence x <= y by A5, YELLOW_0:def 10; :: thesis: verum

end;

assume A6: x is_<=_than F ; :: thesis: x is_<=_than X
let y be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not y in X or x <= y )
assume y in X ; :: thesis: x <= y
then {y} c= X by ZFMISC_1:37;
then ( inf {y} in F & ex_inf_of {y},L ) by A1, A3;
then A7: ( {y} is_>=_than inf {y} & inf {y} >= x ) by A6, LATTICE3:def 8, YELLOW_0:def 10;
then y >= inf {y} by YELLOW_0:7;
hence x <= y by A7, ORDERS_2:26; :: thesis: verum