reconsider f = the carrier of R --> p as Function of R,T ;
take NetStr(# the carrier of R, the InternalRel of R,f #) ; :: thesis: ( RelStr(# the carrier of NetStr(# the carrier of R, the InternalRel of R,f #), the InternalRel of NetStr(# the carrier of R, the InternalRel of R,f #) #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of NetStr(# the carrier of R, the InternalRel of R,f #) = the carrier of NetStr(# the carrier of R, the InternalRel of R,f #) --> p )
thus ( RelStr(# the carrier of NetStr(# the carrier of R, the InternalRel of R,f #), the InternalRel of NetStr(# the carrier of R, the InternalRel of R,f #) #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of NetStr(# the carrier of R, the InternalRel of R,f #) = the carrier of NetStr(# the carrier of R, the InternalRel of R,f #) --> p ) ; :: thesis: verum