let L be non empty reflexive transitive RelStr ; :: thesis: for X being Subset of L holds
( ex_inf_of X,L iff ex_inf_of uparrow X,L )
let X be Subset of L; :: thesis: ( ex_inf_of X,L iff ex_inf_of uparrow X,L )
for x being Element of L 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