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