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

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