let A be non trivial set ; :: thesis: not IdPrefSpace A is preference-like
set X = IdPrefSpace A;
A1: the PrefRel of (IdPrefSpace A) = {} by Def5;
A3: the ToleranceRel of (IdPrefSpace A) = id A by Def5;
A5: the InternalRel of (IdPrefSpace A) = {} by Def5;
S1: (( the PrefRel of (IdPrefSpace A) \/ ( the PrefRel of (IdPrefSpace A) ~)) \/ the ToleranceRel of (IdPrefSpace A)) \/ the InternalRel of (IdPrefSpace A) = ((({} (A,A)) \/ ({} (A,A))) \/ (id A)) \/ ({} (A,A)) by A1, A3, A5
.= id A ;
A = the carrier of (IdPrefSpace A) by Def5;
hence not IdPrefSpace A is preference-like by ROUGHS_1:1, S1; :: thesis: verum