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 #)
; ( 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 )
; verum