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
for a1, b1 being Element of P1
for a2, b2 being Element of P2 st a1 = a2 & b1 = b2 holds
( ( a1 <= b1 implies a2 <= b2 ) & ( a1 < b1 implies a2 < b2 ) )