let X be PreferenceStr ; :: thesis: ( X is empty implies X is preference-like )
assume A1: X is empty ; :: thesis: X is preference-like
then the PrefRel of X /\ the InternalRel of X = {} ;
then the PrefRel of X misses the InternalRel of X by XBOOLE_0:def 7;
then A3: the PrefRel of X, the ToleranceRel of X, the InternalRel of X are_mutually_disjoint by A1;
s1: the PrefRel of X = {} by A1;
s2: the PrefRel of X ~ = {} by A1;
the InternalRel of X = {} by A1;
hence X is preference-like by A1, A3, s1, s2; :: thesis: verum