let A be 2 -element set ; for a, b being Element of A st a <> b holds
( not IntPrefSpace (A,a,b) is empty & IntPrefSpace (A,a,b) is preference-like )
let a, b be Element of A; ( a <> b implies ( not IntPrefSpace (A,a,b) is empty & IntPrefSpace (A,a,b) is preference-like ) )
assume Z1:
a <> b
; ( not IntPrefSpace (A,a,b) is empty & IntPrefSpace (A,a,b) is preference-like )
set X = IntPrefSpace (A,a,b);
a3: the ToleranceRel of (IntPrefSpace (A,a,b)) =
{[a,a],[b,b]}
by Def4
.=
id A
by Lemma4, Z1
.=
id the carrier of (IntPrefSpace (A,a,b))
by Def4
;
a4:
the InternalRel of (IntPrefSpace (A,a,b)) = {[a,b],[b,a]}
by Def4;
( the PrefRel of (IntPrefSpace (A,a,b)) = {} (A,A) & the ToleranceRel of (IntPrefSpace (A,a,b)) = {[a,a],[b,b]} & the InternalRel of (IntPrefSpace (A,a,b)) = {[a,b],[b,a]} )
by Def4;
then
( the PrefRel of (IntPrefSpace (A,a,b)) /\ the InternalRel of (IntPrefSpace (A,a,b)) = {} & the ToleranceRel of (IntPrefSpace (A,a,b)) /\ the InternalRel of (IntPrefSpace (A,a,b)) = {} & the PrefRel of (IntPrefSpace (A,a,b)) /\ the ToleranceRel of (IntPrefSpace (A,a,b)) = {} )
by Z1, Lemma11, XBOOLE_0:def 7;
then A5:
the PrefRel of (IntPrefSpace (A,a,b)), the ToleranceRel of (IntPrefSpace (A,a,b)), the InternalRel of (IntPrefSpace (A,a,b)) are_mutually_disjoint
by XBOOLE_0:def 7;
C4:
the PrefRel of (IntPrefSpace (A,a,b)) = {} (A,A)
by Def4;
C6:
the ToleranceRel of (IntPrefSpace (A,a,b)) = {[a,a],[b,b]}
by Def4;
C1:
the carrier of (IntPrefSpace (A,a,b)) = A
by Def4;
C2:
the InternalRel of (IntPrefSpace (A,a,b)) = {[a,b],[b,a]}
by Def4;
D1:
A = {a,b}
by Z1, Lemma3;
(( the PrefRel of (IntPrefSpace (A,a,b)) \/ ( the PrefRel of (IntPrefSpace (A,a,b)) ~)) \/ the ToleranceRel of (IntPrefSpace (A,a,b))) \/ the InternalRel of (IntPrefSpace (A,a,b)) =
((({} (A,A)) \/ ({} (A,A))) \/ {[a,a],[b,b]}) \/ {[a,b],[b,a]}
by C2, C4, C6
.=
{[a,a],[a,b],[b,a],[b,b]}
by Lemma10
.=
nabla the carrier of (IntPrefSpace (A,a,b))
by C1, D1, ZFMISC_1:122
;
hence
( not IntPrefSpace (A,a,b) is empty & IntPrefSpace (A,a,b) is preference-like )
by Def4, a3, a4, A5, Lemma9, Z1; verum