let P be non empty PIStr ; :: thesis: ( P is PI-preference-like implies the PrefRel of P = (CharRel P) /\ (((CharRel P) ~) `) )
assume A1: P is PI-preference-like ; :: thesis: the PrefRel 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 PrefRel of P iff [x,y] in (CharRel P) /\ (((CharRel P) ~) `) )

proof

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

proof

assume Z0: [x,y] in the PrefRel of P ; :: thesis: [x,y] in (CharRel P) /\ (((CharRel P) ~) `)
then k1: ( x in field the PrefRel of P & y in field the PrefRel of P ) by RELAT_1:15;
Z1: not [x,y] in the ToleranceRel of P by Z0, XBOOLE_0:def 4, A1;
( ( [x,y] in the PrefRel of P or [x,y] in the ToleranceRel of P ) & not [y,x] in the PrefRel of P & not [y,x] in the ToleranceRel of P ) by LemAsym, Z0, A1, Z1, LemSym;
then cc: ( [x,y] in the PrefRel of P \/ the ToleranceRel of P & not [y,x] in the PrefRel of P \/ the ToleranceRel of P ) by XBOOLE_0:def 3;
then ( [x,y] in CharRel P & 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 XBOOLE_0:def 4, cc; :: thesis: verum

end;

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

proof

assume cc: [x,y] in (CharRel P) /\ (((CharRel P) ~) `) ; :: thesis: [x,y] in the PrefRel of P
then ( [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 ( [x,y] in CharRel P & not [y,x] in CharRel P ) by RELAT_1:def 7, cc, XBOOLE_0:def 4;
then ( ( [x,y] in the PrefRel of P & not [y,x] in the PrefRel of P & not [y,x] in the ToleranceRel of P ) or ( [x,y] in the ToleranceRel of P & not [y,x] in the PrefRel of P & not [y,x] in the ToleranceRel of P ) ) by XBOOLE_0:def 3;
hence [x,y] in the PrefRel of P by LemSym, A1; :: thesis: verum

end;

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

end;

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