let x, y, z be set ; :: 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 & y in NAT & 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 & y = y1 ) by A3, ZFMISC_1:33;
consider y2, z2 being Element of NAT such that
A6: [y,z] = [y2,z2] and
A7: y2 <= z2 by A2;
A8: ( y = y2 & z = z2 ) by A6, ZFMISC_1:33;
then x1 <= z2 by A4, A5, A7, XXREAL_0:2;
hence [x,z] in NATOrd by A5, A8; :: thesis: verum