let x, y, z be Element of (N | i); :: according to YELLOW_0:def 2 :: thesis: ( not x <= y or not y <= z or x <= z )
assume A1: ( x <= y & y <= z ) ; :: thesis: x <= z
A2: N | i is full SubNetStr of N by Th14;
consider x1 being Element of N such that
A3: x1 = x and
i <= x1 by Def7;
consider y1 being Element of N such that
A4: y1 = y and
i <= y1 by Def7;
consider z1 being Element of N such that
A5: z1 = z and
i <= z1 by Def7;
( x1 <= y1 & y1 <= z1 ) by A1, A2, A3, A4, A5, YELLOW_6:20;
then x1 <= z1 by YELLOW_0:def 2;
hence x <= z by A2, A3, A5, YELLOW_6:21; :: thesis: verum