let L be non empty transitive RelStr ; :: thesis: for S being non empty sups-closed Subset of
for X being Subset of st ex_sup_of X,L holds
( ex_sup_of X, subrelstr S & "\/" X,(subrelstr S) = "\/" X,L )
let S be non empty sups-closed Subset of ; :: thesis: for X being Subset of st ex_sup_of X,L holds
( ex_sup_of X, subrelstr S & "\/" X,(subrelstr S) = "\/" X,L )
let X be Subset of ; :: thesis: ( ex_sup_of X,L implies ( ex_sup_of X, subrelstr S & "\/" X,(subrelstr S) = "\/" X,L ) )
A1: X is Subset of by YELLOW_0:def 15;
assume A2: ex_sup_of X,L ; :: thesis: ( ex_sup_of X, subrelstr S & "\/" X,(subrelstr S) = "\/" X,L )
subrelstr S is non empty full sups-inheriting SubRelStr of L by Def4;
then "\/" X,L in the carrier of (subrelstr S) by A1, A2, YELLOW_0:def 19;
hence ( ex_sup_of X, subrelstr S & "\/" X,(subrelstr S) = "\/" X,L ) by A1, A2, YELLOW_0:65; :: thesis: verum