let P be pcs-Str ; :: thesis: for a being set holds
( the carrier of P c= the carrier of (pcs-extension P,a) & the InternalRel of P c= the InternalRel of (pcs-extension P,a) & the ToleranceRel of P c= the ToleranceRel of (pcs-extension P,a) )
let a be set ; :: thesis: ( the carrier of P c= the carrier of (pcs-extension P,a) & the InternalRel of P c= the InternalRel of (pcs-extension P,a) & the ToleranceRel of P c= the ToleranceRel of (pcs-extension P,a) )
set R = pcs-extension P,a;
A1: the carrier of (pcs-extension P,a) = {a} \/ the carrier of P by Def39;
A2: the InternalRel of (pcs-extension P,a) = [:{a},the carrier of (pcs-extension P,a):] \/ the InternalRel of P by Def39;
the ToleranceRel of (pcs-extension P,a) = ([:{a},the carrier of (pcs-extension P,a):] \/ [:the carrier of (pcs-extension P,a),{a}:]) \/ the ToleranceRel of P by Def39;
hence ( the carrier of P c= the carrier of (pcs-extension P,a) & the InternalRel of P c= the InternalRel of (pcs-extension P,a) & the ToleranceRel of P c= the ToleranceRel of (pcs-extension P,a) ) by A1, A2, XBOOLE_1:7; :: thesis: verum