let X be PreferenceStr ; ( X is empty implies X is preference-like )
assume A1:
X is empty
; 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; verum