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:64; :: 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