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