let L be non empty 1-sorted ; :: thesis: for N being non empty NetStr over L
for i being Element of N holds N | i is full SubNetStr of N
let N be non empty NetStr over L; :: thesis: for i being Element of N holds N | i is full SubNetStr of N
let i be Element of N; :: thesis: N | i is full SubNetStr of N
A1: the mapping of (N | i) = the mapping of N | the carrier of (N | i) by Def7;
the InternalRel of (N | i) = the InternalRel of N |_2 the carrier of (N | i) by Def7;
then A2: the InternalRel of (N | i) c= the InternalRel of N by XBOOLE_1:17;
the carrier of (N | i) c= the carrier of N by Th13;
then N | i is SubRelStr of N by A2, YELLOW_0:def 13;
then reconsider K = N | i as SubNetStr of N by A1, YELLOW_6:def 6;
the InternalRel of K = the InternalRel of N |_2 the carrier of K by Def7;
then K is full SubRelStr of N by YELLOW_0:def 14, YELLOW_6:def 6;
hence N | i is full SubNetStr of N by YELLOW_6:def 7; :: thesis: verum