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