take NetStr(# the carrier of L,the InternalRel of L,(id L) #) ; :: thesis: ( RelStr(# the carrier of NetStr(# the carrier of L,the InternalRel of L,(id L) #),the InternalRel of NetStr(# the carrier of L,the InternalRel of L,(id L) #) #) = RelStr(# the carrier of L,the InternalRel of L #) & the mapping of NetStr(# the carrier of L,the InternalRel of L,(id L) #) = id L )
thus ( RelStr(# the carrier of NetStr(# the carrier of L,the InternalRel of L,(id L) #),the InternalRel of NetStr(# the carrier of L,the InternalRel of L,(id L) #) #) = RelStr(# the carrier of L,the InternalRel of L #) & the mapping of NetStr(# the carrier of L,the InternalRel of L,(id L) #) = id L ) ; :: thesis: verum