theorem Th4: :: BAGORD_2:17

for N being multLoopStr
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