let L be non empty reflexive transitive RelStr ; :: thesis: for X being Subset of L st ex_sup_of X,L holds

sup X = sup (downarrow X)

let X be Subset of L; :: thesis: ( ex_sup_of X,L implies sup X = sup (downarrow X) )

for x being Element of L holds

( x is_>=_than X iff x is_>=_than downarrow X ) by Th31;

hence ( ex_sup_of X,L implies sup X = sup (downarrow X) ) by YELLOW_0:47; :: thesis: verum

sup X = sup (downarrow X)

let X be Subset of L; :: thesis: ( ex_sup_of X,L implies sup X = sup (downarrow X) )

for x being Element of L holds

( x is_>=_than X iff x is_>=_than downarrow X ) by Th31;

hence ( ex_sup_of X,L implies sup X = sup (downarrow X) ) by YELLOW_0:47; :: thesis: verum