let L be non empty reflexive transitive RelStr ; :: thesis: for X being Subset of holds
( ex_inf_of X,L iff ex_inf_of uparrow X,L )
let X be Subset of ; :: thesis: ( ex_inf_of X,L iff ex_inf_of uparrow X,L )
for x being Element of holds
( x is_<=_than X iff x is_<=_than uparrow X ) by Th36;
hence ( ex_inf_of X,L iff ex_inf_of uparrow X,L ) by YELLOW_0:48; :: thesis: verum