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 ) ) )
( ( a1 <= b1 implies [a1,b1] in the InternalRel of P1 ) & ( [a1,b1] in the InternalRel of P1 implies a1 <= b1 ) & ( a2 <= b2 implies [a2,b2] in the InternalRel of P2 ) & ( [a2,b2] in the InternalRel of P2 implies a2 <= b2 ) ) by ORDERS_2:def 9;
hence ( a1 = a2 & b1 = b2 implies ( ( a1 <= b1 implies a2 <= b2 ) & ( a1 < b1 implies a2 < b2 ) ) ) by A1, ORDERS_2:def 10; :: thesis: verum