e in {e} by TARSKI:def 1;
then reconsider r = {[e,e]} as Relation of {e} by RELSET_1:3;
A1: dom (id {e}) = {e} by RELAT_1:45;
rng (id {e}) = {e} by RELAT_1:45;
then reconsider f = id {e} as Function of {e}, the carrier of S by A1, RELSET_1:4;
take NetStr(# {e},r,f #) ; :: thesis: ( the carrier of NetStr(# {e},r,f #) = {e} & the InternalRel of NetStr(# {e},r,f #) = {[e,e]} & the mapping of NetStr(# {e},r,f #) = id {e} )
thus ( the carrier of NetStr(# {e},r,f #) = {e} & the InternalRel of NetStr(# {e},r,f #) = {[e,e]} & the mapping of NetStr(# {e},r,f #) = id {e} ) ; :: thesis: verum