:: deftheorem Def40 defines pcs-reverse PCS_0:def 41 :
for P being pcs-Str
for b₂ being strict pcs-Str holds
( b₂ = pcs-reverse P iff ( the carrier of b₂ = the carrier of P & the InternalRel of b₂ = the InternalRel of P ~ & the ToleranceRel of b₂ = the ToleranceRel of P ` ) );