reconsider M = NetStr(# the carrier of R, the InternalRel of R,f #) as non empty strict NetStr over S ;
take M ; :: thesis: ( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of M = f )
thus ( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of M = f ) ; :: thesis: verum