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 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

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
A6: x1 = x and
A7: i <= x1 by Def7;
consider y1 being Element of N such that
A8: y1 = y and
i <= y1 by Def7;
consider z1 being Element of N such that
A9: ( x1 <= z1 & y1 <= z1 ) by YELLOW_6:def 5;
i <= z1 by A7, A9, 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 A6, A8, A9, YELLOW_6:21; :: thesis: verum

end;

hence N | i is directed by YELLOW_6:def 5; :: thesis: verum