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

( 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