let L1, L2 be RelStr ; :: thesis: 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
let A be Subset of L1; :: thesis: 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
let J be Subset of L2; :: thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & A = J implies subrelstr A = subrelstr J )
assume that
A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and
A2: A = J ; :: thesis: subrelstr A = subrelstr J
A3: the carrier of (subrelstr A) = A by YELLOW_0:def 15
.= the carrier of (subrelstr J) by A2, YELLOW_0:def 15 ;
then the InternalRel of (subrelstr A) = the InternalRel of L2 |_2 the carrier of (subrelstr J) by A1, YELLOW_0:def 14
.= the InternalRel of (subrelstr J) by YELLOW_0:def 14 ;
hence subrelstr A = subrelstr J by A3; :: thesis: verum