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) = { y where y is Element of N : i <= y }
let N be non empty NetStr over L; :: thesis: for i being Element of N holds the carrier of (N | i) = { y where y is Element of N : i <= y }
let i be Element of N; :: thesis: the carrier of (N | i) = { y where y is Element of N : i <= y }
thus the carrier of (N | i) c= { y where y is Element of N : i <= y } :: according to XBOOLE_0:def 10 :: thesis: { y where y is Element of N : i <= y } c= the carrier of (N | i)

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in the carrier of (N | i) or q in { y where y is Element of N : i <= y } )
assume q in the carrier of (N | i) ; :: thesis: q in { y where y is Element of N : i <= y }
then ex y being Element of N st
( y = q & i <= y ) by Def7;
hence q in { y where y is Element of N : i <= y } ; :: thesis: verum

end;

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in { y where y is Element of N : i <= y } or q in the carrier of (N | i) )
assume q in { y where y is Element of N : i <= y } ; :: thesis: q in the carrier of (N | i)
then ex y being Element of N st
( q = y & i <= y ) ;
hence q in the carrier of (N | i) by Def7; :: thesis: verum