:: deftheorem PrefDef defines preference-like PREFER_1:def 3 :
for X being PreferenceStr holds
( X is preference-like iff ( the PrefRel of X is asymmetric & the ToleranceRel of X is Tolerance of the carrier of X & the InternalRel of X is irreflexive & the InternalRel of X is symmetric & the PrefRel of X, the ToleranceRel of X, the InternalRel of X are_mutually_disjoint & (( the PrefRel of X \/ ( the PrefRel of X ~)) \/ the ToleranceRel of X) \/ the InternalRel of X = nabla the carrier of X ) );