let L be non empty 1-sorted ; :: thesis: for N being non empty NetStr over L
for i being Element of N holds the carrier of (N | i) c= the carrier of N
let N be non empty NetStr over 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 object ; :: 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 ex y being Element of N st
( y = x & i <= y ) by Def7;
hence x in the carrier of N ; :: thesis: verum