let P be non empty PreferenceStr ; :: thesis: ( P is preference-like implies the ToleranceRel of P = (CharRel P) /\ ((CharRel P) ~) )
assume A1: P is preference-like ; :: thesis: the ToleranceRel of P = (CharRel P) /\ ((CharRel P) ~)
set R = the PrefRel of P;
set T = the ToleranceRel of P;
set C = CharRel P;
for x, y being object holds
( [x,y] in the ToleranceRel of P iff [x,y] in (CharRel P) /\ ((CharRel P) ~) )

proof

let x, y be object ; :: thesis: ( [x,y] in the ToleranceRel of P iff [x,y] in (CharRel P) /\ ((CharRel P) ~) )
Z1: ( [x,y] in the ToleranceRel of P implies [x,y] in (CharRel P) /\ ((CharRel P) ~) )

proof

assume A3: [x,y] in the ToleranceRel of P ; :: thesis: [x,y] in (CharRel P) /\ ((CharRel P) ~)
then A2: ( x in field the ToleranceRel of P & y in field the ToleranceRel of P ) by RELAT_1:15;
( [x,y] in the ToleranceRel of P & [y,x] in the ToleranceRel of P ) by A1, A3, A2, RELAT_2:def 3, RELAT_2:def 11;
then ( [x,y] in the PrefRel of P \/ the ToleranceRel of P & [y,x] in the PrefRel of P \/ the ToleranceRel of P ) by XBOOLE_0:def 3;
then ( [x,y] in CharRel P & [x,y] in (CharRel P) ~ ) by RELAT_1:def 7;
hence [x,y] in (CharRel P) /\ ((CharRel P) ~) by XBOOLE_0:def 4; :: thesis: verum

end;

( [x,y] in (CharRel P) /\ ((CharRel P) ~) implies [x,y] in the ToleranceRel of P )

proof

assume [x,y] in (CharRel P) /\ ((CharRel P) ~) ; :: thesis: [x,y] in the ToleranceRel of P
then ( [x,y] in CharRel P & [x,y] in (CharRel P) ~ ) by XBOOLE_0:def 4;
then ( [x,y] in the PrefRel of P \/ the ToleranceRel of P & [y,x] in the PrefRel of P \/ the ToleranceRel of P ) by RELAT_1:def 7;
then ( ( [x,y] in the PrefRel of P & [y,x] in the PrefRel of P ) or ( [x,y] in the PrefRel of P & [y,x] in the ToleranceRel of P ) or ( [x,y] in the ToleranceRel of P & [y,x] in the PrefRel of P ) or ( [x,y] in the ToleranceRel of P & [y,x] in the ToleranceRel of P ) ) by XBOOLE_0:def 3;
hence [x,y] in the ToleranceRel of P by LemSym, A1, LemAsym; :: thesis: verum

end;

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

end;

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