let A be 2 -element set ; for a, b being Element of A st a <> b holds
PrefSpace (A,a,b) is preference-like
let a, b be Element of A; ( a <> b implies PrefSpace (A,a,b) is preference-like )
assume Z1:
a <> b
; PrefSpace (A,a,b) is preference-like
set X = PrefSpace (A,a,b);
a2:
the PrefRel of (PrefSpace (A,a,b)) = {[a,b]}
by Def3;
a3: the ToleranceRel of (PrefSpace (A,a,b)) =
{[a,a],[b,b]}
by Def3
.=
id A
by Lemma4, Z1
.=
id the carrier of (PrefSpace (A,a,b))
by Def3
;
( the PrefRel of (PrefSpace (A,a,b)) = {[a,b]} & the ToleranceRel of (PrefSpace (A,a,b)) = {[a,a],[b,b]} & the InternalRel of (PrefSpace (A,a,b)) = {} (A,A) )
by Def3;
then
( the PrefRel of (PrefSpace (A,a,b)) /\ the InternalRel of (PrefSpace (A,a,b)) = {} & the ToleranceRel of (PrefSpace (A,a,b)) /\ the InternalRel of (PrefSpace (A,a,b)) = {} & the PrefRel of (PrefSpace (A,a,b)) /\ the ToleranceRel of (PrefSpace (A,a,b)) = {} )
by XBOOLE_0:def 7, Z1, Lemma8;
then A5:
the PrefRel of (PrefSpace (A,a,b)), the ToleranceRel of (PrefSpace (A,a,b)), the InternalRel of (PrefSpace (A,a,b)) are_mutually_disjoint
by XBOOLE_0:def 7;
C4:
the PrefRel of (PrefSpace (A,a,b)) = {[a,b]}
by Def3;
then C5:
the PrefRel of (PrefSpace (A,a,b)) ~ = {[b,a]}
by Lemma7;
C6:
the ToleranceRel of (PrefSpace (A,a,b)) = {[a,a],[b,b]}
by Def3;
C1:
the carrier of (PrefSpace (A,a,b)) = A
by Def3;
D1:
A = {a,b}
by Z1, Lemma3;
(( the PrefRel of (PrefSpace (A,a,b)) \/ ( the PrefRel of (PrefSpace (A,a,b)) ~)) \/ the ToleranceRel of (PrefSpace (A,a,b))) \/ the InternalRel of (PrefSpace (A,a,b)) =
(({[a,b]} \/ {[b,a]}) \/ {[a,a],[b,b]}) \/ ({} (A,A))
by Def3, C4, C5, C6
.=
{[a,a],[a,b],[b,a],[b,b]}
by Lemma6
.=
nabla the carrier of (PrefSpace (A,a,b))
by C1, D1, ZFMISC_1:122
;
hence
PrefSpace (A,a,b) is preference-like
by a2, a3, A5, Def3, Lemma5, Z1; verum