let P be non empty PreferenceStr ; :: thesis: ( P is preference-like implies the InternalRel of P = ((CharRel P) `) /\ (((CharRel P) ~) `) )
assume A1: P is preference-like ; :: thesis: 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 ; :: thesis: ( [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 ; :: thesis: [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; :: thesis: 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) ~) `) ; :: thesis: [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; :: thesis: verum

end;

hence ( [x,y] in the InternalRel of P iff [x,y] in ((CharRel P) `) /\ (((CharRel P) ~) `) ) by Z1; :: thesis: verum

end;

hence the InternalRel of P = ((CharRel P) `) /\ (((CharRel P) ~) `) by RELAT_1:def 2; :: thesis: verum