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