let L be non empty reflexive transitive RelStr ; :: thesis: for X being Subset of L st ex_inf_of X,L holds
inf X = inf (uparrow X)
let X be Subset of L; :: thesis: ( ex_inf_of X,L implies inf X = inf (uparrow X) )
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 implies inf X = inf (uparrow X) ) by YELLOW_0:49; :: thesis: verum