:: deftheorem Def39 defines pcs-extension PCS_0:def 40 :
for P being pcs-Str
for a being set
for b₃ being strict pcs-Str holds
( b₃ = pcs-extension (P,a) iff ( the carrier of b₃ = {a} \/ the carrier of P & the InternalRel of b₃ = [:{a}, the carrier of b₃:] \/ the InternalRel of P & the ToleranceRel of b₃ = ([:{a}, the carrier of b₃:] \/ [: the carrier of b₃,{a}:]) \/ the ToleranceRel of P ) );