theorem :: LATWAL_2:19

for P being non empty pcs-Str st the ToleranceRel of P = id the carrier of P holds
P is pcs-Compatible