let A be non empty set ; :: thesis: for R being total reflexive Relation of A holds CharPrefSpace R is preference-like
let R be total reflexive Relation of A; :: thesis: CharPrefSpace R is preference-like
set X = CharPrefSpace R;
set P = CharPrefSpace R;
XX: ( the carrier of (CharPrefSpace R) = A & the PrefRel of (CharPrefSpace R) = R /\ ((R ~) `) & the ToleranceRel of (CharPrefSpace R) = R /\ (R ~) & the InternalRel of (CharPrefSpace R) = Aux R ) by Def55;
thus CharPrefSpace R is preference-like by LEM1, XX, SumNabla2, MutuDis2, LEM3b, LEM2a; :: thesis: verum