theorem Th21: :: PCS_0:21

for P being pcs-Str
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)) )