let T1, T2 be non empty RelStr ; :: thesis: for S1 being non empty full SubRelStr of T1
for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1,the InternalRel of T1 #) = RelStr(# the carrier of T2,the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is infs-inheriting holds
S2 is infs-inheriting
let S1 be non empty full SubRelStr of T1; :: thesis: for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1,the InternalRel of T1 #) = RelStr(# the carrier of T2,the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is infs-inheriting holds
S2 is infs-inheriting
let S2 be non empty full SubRelStr of T2; :: thesis: ( RelStr(# the carrier of T1,the InternalRel of T1 #) = RelStr(# the carrier of T2,the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is infs-inheriting implies S2 is infs-inheriting )
assume A1: RelStr(# the carrier of T1,the InternalRel of T1 #) = RelStr(# the carrier of T2,the InternalRel of T2 #) ; :: thesis: ( not the carrier of S1 = the carrier of S2 or not S1 is infs-inheriting or S2 is infs-inheriting )
assume A2: the carrier of S1 = the carrier of S2 ; :: thesis: ( not S1 is infs-inheriting or S2 is infs-inheriting )
assume A3: for X being Subset of S1 st ex_inf_of X,T1 holds
"/\" X,T1 in the carrier of S1 ; :: according to YELLOW_0:def 18 :: thesis: S2 is infs-inheriting
let X be Subset of S2; :: according to YELLOW_0:def 18 :: thesis: ( not ex_inf_of X,T2 or "/\" X,T2 in the carrier of S2 )
reconsider Y = X as Subset of S1 by A2;
assume A4: ex_inf_of X,T2 ; :: thesis: "/\" X,T2 in the carrier of S2
then ex_inf_of Y,T1 by A1, YELLOW_0:14;
then "/\" Y,T1 in the carrier of S1 by A3;
hence "/\" X,T2 in the carrier of S2 by A1, A2, A4, YELLOW_0:27; :: thesis: verum