let A be non empty set ; :: thesis: ( not PrefSpace A is empty & PrefSpace A is preference-like )
set X = PrefSpace A;
( the PrefRel of (PrefSpace A) \/ the ToleranceRel of (PrefSpace A)) \/ the InternalRel of (PrefSpace A) = nabla the carrier of (PrefSpace A) ;
hence ( not PrefSpace A is empty & PrefSpace A is preference-like ) by Lemma1; :: thesis: verum