set D = {a} \/ the carrier of P;
set IR = [:{a},({a} \/ the carrier of P):] \/ the InternalRel of P;
set TR = ([:({a} \/ the carrier of P),{a}:] \/ [:{a},({a} \/ the carrier of P):]) \/ the ToleranceRel of P;
A1: {a} c= {a} \/ the carrier of P by XBOOLE_1:7;
then A2: [:{a},({a} \/ the carrier of P):] c= [:({a} \/ the carrier of P),({a} \/ the carrier of P):] by ZFMISC_1:95;
the carrier of P c= {a} \/ the carrier of P by XBOOLE_1:7;
then A3: [: the carrier of P, the carrier of P:] c= [:({a} \/ the carrier of P),({a} \/ the carrier of P):] by ZFMISC_1:96;
then the InternalRel of P c= [:({a} \/ the carrier of P),({a} \/ the carrier of P):] ;
then reconsider IR = [:{a},({a} \/ the carrier of P):] \/ the InternalRel of P as Relation of ({a} \/ the carrier of P) by A2, XBOOLE_1:8;
[:({a} \/ the carrier of P),{a}:] c= [:({a} \/ the carrier of P),({a} \/ the carrier of P):] by A1, ZFMISC_1:95;
then A4: [:({a} \/ the carrier of P),{a}:] \/ [:{a},({a} \/ the carrier of P):] c= [:({a} \/ the carrier of P),({a} \/ the carrier of P):] by A2, XBOOLE_1:8;
the ToleranceRel of P c= [:({a} \/ the carrier of P),({a} \/ the carrier of P):] by A3;
then reconsider TR = ([:({a} \/ the carrier of P),{a}:] \/ [:{a},({a} \/ the carrier of P):]) \/ the ToleranceRel of P as Relation of ({a} \/ the carrier of P) by A4, XBOOLE_1:8;
take pcs-Str(# ({a} \/ the carrier of P),IR,TR #) ; :: thesis: ( the carrier of pcs-Str(# ({a} \/ the carrier of P),IR,TR #) = {a} \/ the carrier of P & the InternalRel of pcs-Str(# ({a} \/ the carrier of P),IR,TR #) = [:{a}, the carrier of pcs-Str(# ({a} \/ the carrier of P),IR,TR #):] \/ the InternalRel of P & the ToleranceRel of pcs-Str(# ({a} \/ the carrier of P),IR,TR #) = ([:{a}, the carrier of pcs-Str(# ({a} \/ the carrier of P),IR,TR #):] \/ [: the carrier of pcs-Str(# ({a} \/ the carrier of P),IR,TR #),{a}:]) \/ the ToleranceRel of P )
thus ( the carrier of pcs-Str(# ({a} \/ the carrier of P),IR,TR #) = {a} \/ the carrier of P & the InternalRel of pcs-Str(# ({a} \/ the carrier of P),IR,TR #) = [:{a}, the carrier of pcs-Str(# ({a} \/ the carrier of P),IR,TR #):] \/ the InternalRel of P & the ToleranceRel of pcs-Str(# ({a} \/ the carrier of P),IR,TR #) = ([:{a}, the carrier of pcs-Str(# ({a} \/ the carrier of P),IR,TR #):] \/ [: the carrier of pcs-Str(# ({a} \/ the carrier of P),IR,TR #),{a}:]) \/ the ToleranceRel of P ) ; :: thesis: verum