let P be non empty PreferenceStr ; ( P is preference-like implies the InternalRel of P = ((CharRel P) `) /\ (((CharRel P) ~) `) )
assume A1:
P is preference-like
; the InternalRel of P = ((CharRel P) `) /\ (((CharRel P) ~) `)
set R = the PrefRel of P;
set T = the ToleranceRel of P;
set I = the InternalRel of P;
set C = CharRel P;
for x, y being object holds
( [x,y] in the InternalRel of P iff [x,y] in ((CharRel P) `) /\ (((CharRel P) ~) `) )
proof
let x,
y be
object ;
( [x,y] in the InternalRel of P iff [x,y] in ((CharRel P) `) /\ (((CharRel P) ~) `) )
Z1:
(
[x,y] in the
InternalRel of
P implies
[x,y] in ((CharRel P) `) /\ (((CharRel P) ~) `) )
proof
assume A3:
[x,y] in the
InternalRel of
P
;
[x,y] in ((CharRel P) `) /\ (((CharRel P) ~) `)
then k1:
(
x in field the
InternalRel of
P &
y in field the
InternalRel of
P )
by RELAT_1:15;
the
PrefRel of
P, the
ToleranceRel of
P, the
InternalRel of
P are_mutually_disjoint
by A1;
then B1:
( the
InternalRel of
P /\ the
ToleranceRel of
P = {} & the
InternalRel of
P /\ the
PrefRel of
P = {} )
by XBOOLE_0:def 7;
then
( ( not
[x,y] in the
InternalRel of
P or not
[x,y] in the
ToleranceRel of
P ) & ( not
[x,y] in the
InternalRel of
P or not
[x,y] in the
PrefRel of
P ) )
by XBOOLE_0:def 4;
then
not
[x,y] in the
PrefRel of
P \/ the
ToleranceRel of
P
by A3, XBOOLE_0:def 3;
then B3:
[x,y] in (CharRel P) `
by Lemma12b, k1;
[y,x] in the
InternalRel of
P
by A3, LemSym, A1;
then
( not
[y,x] in the
ToleranceRel of
P & not
[y,x] in the
PrefRel of
P )
by B1, XBOOLE_0:def 4;
then
not
[y,x] in the
PrefRel of
P \/ the
ToleranceRel of
P
by XBOOLE_0:def 3;
then
not
[x,y] in (CharRel P) ~
by RELAT_1:def 7;
then
[x,y] in ((CharRel P) ~) `
by Lemma12b, k1;
hence
[x,y] in ((CharRel P) `) /\ (((CharRel P) ~) `)
by B3, XBOOLE_0:def 4;
verum
end;
(
[x,y] in ((CharRel P) `) /\ (((CharRel P) ~) `) implies
[x,y] in the
InternalRel of
P )
proof
assume c0:
[x,y] in ((CharRel P) `) /\ (((CharRel P) ~) `)
;
[x,y] in the InternalRel of P
then c1:
(
[x,y] in (CharRel P) ` &
[x,y] in ((CharRel P) ~) ` )
by XBOOLE_0:def 4;
then
not
[x,y] in CharRel P
by XBOOLE_0:def 5;
then J2:
( not
[x,y] in the
PrefRel of
P & not
[x,y] in the
ToleranceRel of
P )
by XBOOLE_0:def 3;
J3:
not
[x,y] in (CharRel P) ~
by XBOOLE_0:def 5, c1;
(CharRel P) ~ = ( the PrefRel of P ~) \/ ( the ToleranceRel of P ~)
by RELAT_1:23;
then
( not
[x,y] in the
PrefRel of
P ~ & not
[x,y] in the
ToleranceRel of
P ~ )
by J3, XBOOLE_0:def 3;
then
not
[x,y] in the
PrefRel of
P \/ ( the PrefRel of P ~)
by XBOOLE_0:def 3, J2;
then
not
[x,y] in ( the PrefRel of P \/ ( the PrefRel of P ~)) \/ the
ToleranceRel of
P
by J2, XBOOLE_0:def 3;
hence
[x,y] in the
InternalRel of
P
by XBOOLE_0:def 3, c0, A1;
verum
end;
hence
(
[x,y] in the
InternalRel of
P iff
[x,y] in ((CharRel P) `) /\ (((CharRel P) ~) `) )
by Z1;
verum
end;
hence
the InternalRel of P = ((CharRel P) `) /\ (((CharRel P) ~) `)
by RELAT_1:def 2; verum