let L be non empty 1-sorted ; :: thesis: for N being net of L
for i being Element of N holds N | i is subnet of N
let N be net of L; :: thesis: for i being Element of N holds N | i is subnet of N
let i be Element of N; :: thesis: N | i is subnet of N
reconsider A = N | i as net of L ;
A1: the carrier of A c= the carrier of N by Th13;
A is subnet of N

proof

reconsider f = id the carrier of A as Function of A,N by A1, FUNCT_2:7;
take f ; :: according to YELLOW_6:def 9 :: thesis: ( the mapping of A = the mapping of N * f & ( for b₁ being Element of the carrier of N ex b₂ being Element of the carrier of A st
for b₃ being Element of the carrier of A holds
( not b₂ <= b₃ or b₁ <= f . b₃ ) ) )
for x being object st x in the carrier of A holds
the mapping of A . x = ( the mapping of N * f) . x

proof

let x be object ; :: thesis: ( x in the carrier of A implies the mapping of A . x = ( the mapping of N * f) . x )
assume A2: x in the carrier of A ; :: thesis: the mapping of A . x = ( the mapping of N * f) . x
thus the mapping of A . x = ( the mapping of N | the carrier of A) . x by Def7
.= the mapping of N . x by A2, FUNCT_1:49
.= the mapping of N . (f . x) by A2, FUNCT_1:18
.= ( the mapping of N * f) . x by A2, FUNCT_2:15 ; :: thesis: verum

end;

hence the mapping of A = the mapping of N * f by FUNCT_2:12; :: thesis: for b₁ being Element of the carrier of N ex b₂ being Element of the carrier of A st
for b₃ being Element of the carrier of A holds
( not b₂ <= b₃ or b₁ <= f . b₃ )
let m be Element of N; :: thesis: ex b₁ being Element of the carrier of A st
for b₂ being Element of the carrier of A holds
( not b₁ <= b₂ or m <= f . b₂ )
consider z being Element of N such that
A3: i <= z and
A4: m <= z by YELLOW_6:def 3;
reconsider n = z as Element of A by A3, Def7;
take n ; :: thesis: for b₁ being Element of the carrier of A holds
( not n <= b₁ or m <= f . b₁ )
let p be Element of A; :: thesis: ( not n <= p or m <= f . p )
assume A5: n <= p ; :: thesis: m <= f . p
reconsider p1 = p as Element of N by A1;
A is SubNetStr of N by Th14;
then z <= p1 by A5, YELLOW_6:11;
then m <= p1 by A4, YELLOW_0:def 2;
hence m <= f . p ; :: thesis: verum

end;

hence N | i is subnet of N ; :: thesis: verum