let T be non empty transitive RelStr ; :: thesis: for S being non empty full SubRelStr of T
for X being Subset of S holds
( S inherits_sup_of X,T iff ( ex_sup_of X,T implies ( ex_sup_of X,S & sup X = "\/" X,T ) ) )
let S be non empty full SubRelStr of T; :: thesis: for X being Subset of S holds
( S inherits_sup_of X,T iff ( ex_sup_of X,T implies ( ex_sup_of X,S & sup X = "\/" X,T ) ) )
let X be Subset of S; :: thesis: ( S inherits_sup_of X,T iff ( ex_sup_of X,T implies ( ex_sup_of X,S & sup X = "\/" X,T ) ) )

hereby :: thesis: ( ( ex_sup_of X,T implies ( ex_sup_of X,S & sup X = "\/" X,T ) ) implies S inherits_sup_of X,T )

assume that
A1: S inherits_sup_of X,T and
A2: ex_sup_of X,T ; :: thesis: ( ex_sup_of X,S & sup X = "\/" X,T )
"\/" X,T in the carrier of S by A1, A2, Def6;
hence ( ex_sup_of X,S & sup X = "\/" X,T ) by A2, YELLOW_0:65; :: thesis: verum

end;

assume A3: ( ex_sup_of X,T implies ( ex_sup_of X,S & sup X = "\/" X,T ) ) ; :: thesis: S inherits_sup_of X,T
assume ex_sup_of X,T ; :: according to YELLOW16:def 6 :: thesis: "\/" X,T in the carrier of S
hence "\/" X,T in the carrier of S by A3; :: thesis: verum