defpred S₁[ set ] means ex y being Element of N st
( y = $1 & i <= y );
consider X being set such that
A1: for x being set holds
( x in X iff ( x in the carrier of N & S₁[x] ) ) from XBOOLE_0:sch 1();
X c= the carrier of N

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in the carrier of N )
assume x in X ; :: thesis: x in the carrier of N
hence x in the carrier of N by A1; :: thesis: verum

end;

then reconsider f = the mapping of N | X as Function of X,the carrier of L by FUNCT_2:38;
set IT = NetStr(# X,(the InternalRel of N |_2 X),f #);
take NetStr(# X,(the InternalRel of N |_2 X),f #) ; :: thesis: ( ( for x being set holds
( x in the carrier of NetStr(# X,(the InternalRel of N |_2 X),f #) iff ex y being Element of N st
( y = x & i <= y ) ) ) & the InternalRel of NetStr(# X,(the InternalRel of N |_2 X),f #) = the InternalRel of N |_2 the carrier of NetStr(# X,(the InternalRel of N |_2 X),f #) & the mapping of NetStr(# X,(the InternalRel of N |_2 X),f #) = the mapping of N | the carrier of NetStr(# X,(the InternalRel of N |_2 X),f #) )
thus for x being set holds
( x in the carrier of NetStr(# X,(the InternalRel of N |_2 X),f #) iff ex y being Element of N st
( y = x & i <= y ) ) by A1; :: thesis: ( the InternalRel of NetStr(# X,(the InternalRel of N |_2 X),f #) = the InternalRel of N |_2 the carrier of NetStr(# X,(the InternalRel of N |_2 X),f #) & the mapping of NetStr(# X,(the InternalRel of N |_2 X),f #) = the mapping of N | the carrier of NetStr(# X,(the InternalRel of N |_2 X),f #) )
thus ( the InternalRel of NetStr(# X,(the InternalRel of N |_2 X),f #) = the InternalRel of N |_2 the carrier of NetStr(# X,(the InternalRel of N |_2 X),f #) & the mapping of NetStr(# X,(the InternalRel of N |_2 X),f #) = the mapping of N | the carrier of NetStr(# X,(the InternalRel of N |_2 X),f #) ) ; :: thesis: verum