reconsider TR = the ToleranceRel of P ` as Relation of the carrier of P ;
take pcs-Str(# the carrier of P,( the InternalRel of P ~),TR #) ; :: thesis: ( the carrier of pcs-Str(# the carrier of P,( the InternalRel of P ~),TR #) = the carrier of P & the InternalRel of pcs-Str(# the carrier of P,( the InternalRel of P ~),TR #) = the InternalRel of P ~ & the ToleranceRel of pcs-Str(# the carrier of P,( the InternalRel of P ~),TR #) = the ToleranceRel of P ` )
thus ( the carrier of pcs-Str(# the carrier of P,( the InternalRel of P ~),TR #) = the carrier of P & the InternalRel of pcs-Str(# the carrier of P,( the InternalRel of P ~),TR #) = the InternalRel of P ~ & the ToleranceRel of pcs-Str(# the carrier of P,( the InternalRel of P ~),TR #) = the ToleranceRel of P ` ) ; :: thesis: verum