let N be multLoopStr ; :: thesis: for M1, M2 being strict RelExtension of N st ( for m, n being Element of M1
for x, y being Element of M2 st m = x & n = y holds
( m <= n iff x <= y ) ) holds
M1 = M2
let M1, M2 be strict RelExtension of N; :: thesis: ( ( for m, n being Element of M1
for x, y being Element of M2 st m = x & n = y holds
( m <= n iff x <= y ) ) implies M1 = M2 )
assume Z4: for m, n being Element of M1
for x, y being Element of M2 st m = x & n = y holds
( m <= n iff x <= y ) ; :: thesis: M1 = M2
A2: ( multLoopStr(# the carrier of M1, the multF of M1, the OneF of M1 #) = multLoopStr(# the carrier of N, the multF of N, the OneF of N #) & multLoopStr(# the carrier of M2, the multF of M2, the OneF of M2 #) = multLoopStr(# the carrier of N, the multF of N, the OneF of N #) ) by RE;
the InternalRel of M1 = the InternalRel of M2
proof
let a be object ; :: according to RELAT_1:def 2 :: thesis: for b1 being object holds
( ( not [a,b1] in the InternalRel of M1 or [a,b1] in the InternalRel of M2 ) & ( not [a,b1] in the InternalRel of M2 or [a,b1] in the InternalRel of M1 ) )
let b be object ; :: thesis: ( ( not [a,b] in the InternalRel of M1 or [a,b] in the InternalRel of M2 ) & ( not [a,b] in the InternalRel of M2 or [a,b] in the InternalRel of M1 ) )
hereby :: thesis: ( not [a,b] in the InternalRel of M2 or [a,b] in the InternalRel of M1 )
assume A3: [a,b] in the InternalRel of M1 ; :: thesis: [a,b] in the InternalRel of M2
then reconsider m = a, n = b as Element of M1 by ZFMISC_1:87;
reconsider x = m, y = n as Element of M2 by A2;
m <= n by A3, ORDERS_2:def 5;
then x <= y by Z4;
hence [a,b] in the InternalRel of M2 by ORDERS_2:def 5; :: thesis: verum
end;
assume A3: [a,b] in the InternalRel of M2 ; :: thesis: [a,b] in the InternalRel of M1
then reconsider m = a, n = b as Element of M2 by ZFMISC_1:87;
reconsider x = m, y = n as Element of M1 by A2;
m <= n by A3, ORDERS_2:def 5;
then x <= y by Z4;
hence [a,b] in the InternalRel of M1 by ORDERS_2:def 5; :: thesis: verum
end;
hence M1 = M2 by A2; :: thesis: verum