let L be non empty reflexive transitive RelStr ; 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; ( ( 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
; ( 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; verum