let L1, L2 be 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
let A be 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 J be Subset of L2; ( 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
; 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; verum