A1: i <= i ;
hence not N | i is empty by Def7; :: thesis: N | i is reflexive
reconsider A = N | i as non empty strict NetStr over L by A1, Def7;
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
A2: y = x and
i <= y by Def7;
( N | i is full SubNetStr of N & y <= y ) by Th14;
hence x <= x by A2, YELLOW_6:12; :: thesis: verum
end;
hence N | i is reflexive ; :: thesis: verum