set X = IdPrefSpace A;
set a = the Element of A;
reconsider C = { the Element of A} as Subset of A ;
s:
A = { the Element of A}
by ZFMISC_1:132;
then B1:
the ToleranceRel of (IdPrefSpace A) = id { the Element of A}
by Def5;
B2:
C = the carrier of (IdPrefSpace A)
by Def5, s;
a5:
( the PrefRel of (IdPrefSpace A) = {} (A,A) & the InternalRel of (IdPrefSpace A) = {} (A,A) )
by Def5;
Z0:
the PrefRel of (IdPrefSpace A) = {} (A,A)
by Def5;
Z1: the ToleranceRel of (IdPrefSpace A) =
{[ the Element of A, the Element of A]}
by B1, SYSREL:13
.=
[:{ the Element of A},{ the Element of A}:]
by ZFMISC_1:29
;
Z2:
the InternalRel of (IdPrefSpace A) = {} (A,A)
by Def5;
(( the PrefRel of (IdPrefSpace A) \/ ( the PrefRel of (IdPrefSpace A) ~)) \/ the ToleranceRel of (IdPrefSpace A)) \/ the InternalRel of (IdPrefSpace A) =
((({} (A,A)) \/ ({} (A,A))) \/ [:{ the Element of A},{ the Element of A}:]) \/ ({} (A,A))
by Z2, Z0, Z1
.=
nabla the carrier of (IdPrefSpace A)
by B2
;
hence
( not IdPrefSpace A is empty & IdPrefSpace A is preference-like )
by B1, B2, a5, Lemma1; verum