let P1, P2 be RelStr ; ( RelStr(# the carrier of P1, the InternalRel of P1 #) = RelStr(# the carrier of P2, the InternalRel of P2 #) implies 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 ) ) )
assume A1:
RelStr(# the carrier of P1, the InternalRel of P1 #) = RelStr(# the carrier of P2, the InternalRel of P2 #)
; 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 ) )
let a1, b1 be 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 ) )
let a2, b2 be Element of P2; ( a1 = a2 & b1 = b2 implies ( ( a1 <= b1 implies a2 <= b2 ) & ( a1 < b1 implies a2 < b2 ) ) )
A2:
( a2 <= b2 iff [a2,b2] in the InternalRel of P2 )
;
( a1 <= b1 iff [a1,b1] in the InternalRel of P1 )
;
hence
( a1 = a2 & b1 = b2 implies ( ( a1 <= b1 implies a2 <= b2 ) & ( a1 < b1 implies a2 < b2 ) ) )
by A1, A2; verum