thus N | i is transitive :: thesis: N | i is directed

proof

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 that
A1: x <= y and
A2: y <= z ; :: thesis: 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; :: thesis: verum

end;

for x, y being Element of (N | i) ex z being Element of (N | i) st
( x <= z & y <= z )

proof

let x, y be Element of (N | i); :: thesis: ex z being Element of (N | i) st
( x <= z & y <= z )
consider x1 being Element of N such that
A8: x1 = x and
A9: i <= x1 by Def7;
consider y1 being Element of N such that
A10: y1 = y and
i <= y1 by Def7;
consider z1 being Element of N such that
A11: x1 <= z1 and
A12: y1 <= z1 by YELLOW_6:def 3;
i <= z1 by A9, A11, YELLOW_0:def 2;
then reconsider z = z1 as Element of (N | i) by Def7;
take z ; :: thesis: ( x <= z & y <= z )
N | i is full SubNetStr of N by Th14;
hence ( x <= z & y <= z ) by A8, A10, A11, A12, YELLOW_6:12; :: thesis: verum

end;

hence N | i is directed ; :: thesis: verum