:: deftheorem Def55 defines CharPrefSpace PREFER_1:def 11 :
for X being set
for P being Relation of X
for b₃ being strict PreferenceStr holds
( b₃ = CharPrefSpace P iff ( the carrier of b₃ = X & the PrefRel of b₃ = P /\ ((P ~) `) & the ToleranceRel of b₃ = P /\ (P ~) & the InternalRel of b₃ = Aux P ) );