theorem Th12: :: WAYBEL21:12

for T1, T2, R being RelStr
for S being SubRelStr of T1 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of R, the InternalRel of R #) holds
( R is SubRelStr of T2 & ( S is full implies R is full SubRelStr of T2 ) )