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:118;
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:119;
then the InternalRel of P c= [:({a} \/ the carrier of P),({a} \/ the carrier of P):] by XBOOLE_1:1;
then [:{a},({a} \/ the carrier of P):] \/ the InternalRel of P c= [:({a} \/ the carrier of P),({a} \/ the carrier of P):] by A2, XBOOLE_1:8;
then reconsider IR = [:{a},({a} \/ the carrier of P):] \/ the InternalRel of P as Relation of ({a} \/ the carrier of P) ;
[:({a} \/ the carrier of P),{a}:] c= [:({a} \/ the carrier of P),({a} \/ the carrier of P):] by A1, ZFMISC_1:118;
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, XBOOLE_1:1;
then ([:({a} \/ the carrier of P),{a}:] \/ [:{a},({a} \/ the carrier of P):]) \/ the ToleranceRel of P c= [:({a} \/ the carrier of P),({a} \/ the carrier of P):] by A4, XBOOLE_1:8;
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) ;
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