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