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