for L being non empty reflexive transitive RelStr
for X being Subset of L holds
( ex_inf_of X,L iff ex_inf_of uparrow X,L )