thus not N | i is empty :: thesis: N | i is reflexive

proof

i <= i ;
then i in the carrier of (N | i) by Def7;
hence not N | i is empty ; :: thesis: verum

end;

then reconsider A = N | i as non empty strict NetStr of L ;
A is reflexive

proof

let x be Element of A; :: according to YELLOW_0:def 1 :: thesis: x <= x
consider y being Element of N such that
A1: y = x and
i <= y by Def7;
A2: N | i is full SubNetStr of N by Th14;
y <= y ;
hence x <= x by A1, A2, YELLOW_6:21; :: thesis: verum

end;

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