:: deftheorem defines CharRel PREFER_1:def 8 :
for P being PIStr holds CharRel P = the PrefRel of P \/ the ToleranceRel of P;