let L be non empty reflexive transitive RelStr ; :: thesis: for X being Subset of st ex_sup_of X,L holds
sup X = sup (downarrow X)
let X be Subset of ; :: thesis: ( ex_sup_of X,L implies sup X = sup (downarrow X) )
for x being Element of 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