let L be non empty 1-sorted ; :: thesis: for N being non empty NetStr of L
for i being Element of N holds the carrier of (N | i) c= the carrier of N
let N be non empty NetStr of L; :: thesis: for i being Element of N holds the carrier of (N | i) c= the carrier of N
let i be Element of N; :: thesis: the carrier of (N | i) c= the carrier of N
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (N | i) or x in the carrier of N )
assume x in the carrier of (N | i) ; :: thesis: x in the carrier of N
then consider y being Element of N such that
A1: y = x and
i <= y by Def7;
thus x in the carrier of N by A1; :: thesis: verum