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