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