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