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_inf_of X,T iff ( ex_inf_of X,T implies ( ex_inf_of X,S & inf X = "/\" X,T ) ) )
let S be non empty full SubRelStr of T; :: thesis: for X being Subset of S holds
( S inherits_inf_of X,T iff ( ex_inf_of X,T implies ( ex_inf_of X,S & inf X = "/\" X,T ) ) )
let X be Subset of S; :: thesis: ( S inherits_inf_of X,T iff ( ex_inf_of X,T implies ( ex_inf_of X,S & inf X = "/\" X,T ) ) )

hereby :: thesis: ( ( ex_inf_of X,T implies ( ex_inf_of X,S & inf X = "/\" X,T ) ) implies S inherits_inf_of X,T )

assume that
A1: S inherits_inf_of X,T and
A2: ex_inf_of X,T ; :: thesis: ( ex_inf_of X,S & inf X = "/\" X,T )
"/\" X,T in the carrier of S by A1, A2, Def7;
hence ( ex_inf_of X,S & inf X = "/\" X,T ) by A2, YELLOW_0:64; :: thesis: verum

end;

assume A3: ( ex_inf_of X,T implies ( ex_inf_of X,S & inf X = "/\" X,T ) ) ; :: thesis: S inherits_inf_of X,T
assume ex_inf_of X,T ; :: according to YELLOW16:def 7 :: thesis: "/\" X,T in the carrier of S
hence "/\" X,T in the carrier of S by A3; :: thesis: verum