theorem :: PREFER_1:41

for P being non empty PIStr st P is PI-preference-like holds
the PrefRel of P = (CharRel P) /\ (((CharRel P) ~) `)