let P1, P2 be RelStr ; :: thesis: ( 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 #) ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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; :: thesis: verum