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

( ex_inf_of X,L iff ex_inf_of F,L )

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 ( ex_inf_of X,L iff ex_inf_of F,L ) )

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: ( ex_inf_of X,L iff ex_inf_of F,L )

for x being Element of L holds

( x is_<=_than X iff x is_<=_than F ) by A1, A2, A3, Th57;

hence ( ex_inf_of X,L iff ex_inf_of F,L ) by YELLOW_0:48; :: 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

( ex_inf_of X,L iff ex_inf_of F,L )

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 ( ex_inf_of X,L iff ex_inf_of F,L ) )

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: ( ex_inf_of X,L iff ex_inf_of F,L )

for x being Element of L holds

( x is_<=_than X iff x is_<=_than F ) by A1, A2, A3, Th57;

hence ( ex_inf_of X,L iff ex_inf_of F,L ) by YELLOW_0:48; :: thesis: verum