for T1, T2 being non empty RelStr
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