let L be non empty reflexive transitive RelStr ; :: thesis: for X being Subset of holds
( ex_sup_of X,L iff ex_sup_of downarrow X,L )
let X be Subset of ; :: thesis: ( ex_sup_of X,L iff ex_sup_of downarrow X,L )
for x being Element of holds
( x is_>=_than X iff x is_>=_than downarrow X ) by Th31;
hence ( ex_sup_of X,L iff ex_sup_of downarrow X,L ) by YELLOW_0:46; :: thesis: verum