theorem :: YELLOW12:16

for L1, L2 being RelStr
for A being Subset of L1
for J being Subset of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & A = J holds
subrelstr A = subrelstr J