:: deftheorem defines c= PCS_0:def 34 :
for P, Q being pcs-Str holds
( P c= Q iff ( the carrier of P c= the carrier of Q & the InternalRel of P c= the InternalRel of Q & the ToleranceRel of P c= the ToleranceRel of Q ) );