for P1, P2 being RelStr st RelStr(# the carrier of P1, the InternalRel of P1 #) = RelStr(# the carrier of P2, the InternalRel of P2 #) holds
( ( P1 is lower-bounded implies P2 is lower-bounded ) & ( P1 is upper-bounded implies P2 is upper-bounded ) ) by Th2;