let x, y be object ; :: according to RELAT_2:def 4 :: thesis: ( not x in NAT or not y in NAT or not [x,y] in NATOrd or not [y,x] in NATOrd or x = y )
assume that
x in NAT and
y in NAT and
A1: [x,y] in NATOrd and
A2: [y,x] in NATOrd ; :: thesis: x = y
consider x9, y9 being Element of NAT such that
A3: [x,y] = [x9,y9] and
A4: x9 <= y9 by A1;
A5: x = x9 by A3, XTUPLE_0:1;
A6: y = y9 by A3, XTUPLE_0:1;
consider y2, x2 being Element of NAT such that
A7: [y,x] = [y2,x2] and
A8: y2 <= x2 by A2;
A9: y2 = y9 by A6, A7, XTUPLE_0:1;
x2 = x9 by A5, A7, XTUPLE_0:1;
hence x = y by A4, A5, A6, A8, A9, XXREAL_0:1; :: thesis: verum