let L be non empty reflexive transitive RelStr ; :: thesis: for X being Subset of L holds
( ex_sup_of X,L iff ex_sup_of downarrow X,L )
let X be Subset of L; :: thesis: ( ex_sup_of X,L iff ex_sup_of downarrow X,L )
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 iff ex_sup_of downarrow X,L ) by YELLOW_0:46; :: thesis: verum