let L be non empty 1-sorted ; :: thesis: for N being non empty NetStr of L
for i being Element of N holds N | i is full SubNetStr of N
let N be non empty NetStr of 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 InternalRel of (N | i) = the InternalRel of N |_2 the carrier of (N | i) by Def7;
A2: N | i is SubRelStr of N

proof

thus the carrier of (N | i) c= the carrier of N by Th13; :: according to YELLOW_0:def 13 :: thesis: the InternalRel of (N | i) c= the InternalRel of N
thus the InternalRel of (N | i) c= the InternalRel of N by A1, XBOOLE_1:17; :: thesis: verum

end;

N | i is SubNetStr of N

proof

thus N | i is SubRelStr of N by A2; :: according to YELLOW_6:def 8 :: thesis: the mapping of (N | i) = the mapping of N | the carrier of (N | i)
thus the mapping of (N | i) = the mapping of N | the carrier of (N | i) by Def7; :: thesis: verum

end;

then reconsider K = N | i as SubNetStr of N ;
K is full

proof

thus K is full SubRelStr of N :: according to YELLOW_6:def 9 :: thesis: verum

proof

the InternalRel of K = the InternalRel of N |_2 the carrier of K by Def7;
hence K is full SubRelStr of N by A2, YELLOW_0:def 14; :: thesis: verum

end;

end;

hence N | i is full SubNetStr of N ; :: thesis: verum