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 )

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 A8: {y} c= X by ZFMISC_1:31;

then A9: inf {y} in F by A3;

ex_inf_of {y},L by A1, A8;

then A10: {y} is_>=_than inf {y} by YELLOW_0:def 10;

A11: inf {y} >= x by A7, A9;

y >= inf {y} by A10, YELLOW_0:7;

hence x <= y by A11, ORDERS_2:3; :: thesis: verum

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 A7:
x is_<=_than F
; :: thesis: x is_<=_than X
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 and

A6: y = "/\" (Y,L) by A2;

x is_<=_than Y by A4;

hence x <= y by A5, A6, YELLOW_0:def 10; :: thesis: verum

end;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 and

A6: y = "/\" (Y,L) by A2;

x is_<=_than Y by A4;

hence x <= y by A5, A6, YELLOW_0:def 10; :: thesis: verum

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 A8: {y} c= X by ZFMISC_1:31;

then A9: inf {y} in F by A3;

ex_inf_of {y},L by A1, A8;

then A10: {y} is_>=_than inf {y} by YELLOW_0:def 10;

A11: inf {y} >= x by A7, A9;

y >= inf {y} by A10, YELLOW_0:7;

hence x <= y by A11, ORDERS_2:3; :: thesis: verum