let X be non empty set ; for R being total reflexive Relation of X holds
( (R `) /\ ((R ~) `) is irreflexive & (R `) /\ ((R ~) `) is symmetric )
let R be total reflexive Relation of X; ( (R `) /\ ((R ~) `) is irreflexive & (R `) /\ ((R ~) `) is symmetric )
A0:
id (field R) c= R
by RELAT_2:1;
A1:
dom R = X
by PARTFUN1:def 2;
then
dom (R ~) = X
by RELAT_2:12;
then
rng R = X
by RELAT_1:20;
then A3:
(id X) /\ (R `) = {}
by XBOOLE_0:def 7, SUBSET_1:24, A0, A1;
(id X) /\ ((R `) /\ ((R ~) `)) = ((id X) /\ (R `)) /\ ((R ~) `)
by XBOOLE_1:16;
then
id X misses (R `) /\ ((R ~) `)
by XBOOLE_0:def 7, A3;
then z1:
id (field ((R `) /\ ((R ~) `))) misses (R `) /\ ((R ~) `)
by XBOOLE_1:63, SYSREL:15;
for x, y being object st [x,y] in (R `) /\ ((R ~) `) holds
[y,x] in (R `) /\ ((R ~) `)
proof
let x,
y be
object ;
( [x,y] in (R `) /\ ((R ~) `) implies [y,x] in (R `) /\ ((R ~) `) )
assume B0:
[x,y] in (R `) /\ ((R ~) `)
;
[y,x] in (R `) /\ ((R ~) `)
then B1:
(
x is
Element of
X &
y is
Element of
X )
by ZFMISC_1:87;
(
[x,y] in R ` &
[x,y] in (R ~) ` )
by XBOOLE_0:def 4, B0;
then
( not
[x,y] in R & not
[x,y] in R ~ )
by XBOOLE_0:def 5;
then
( not
[y,x] in R ~ & not
[y,x] in R )
by RELAT_1:def 7;
then
(
[y,x] in (R ~) ` &
[y,x] in R ` )
by Lemma12b, B1;
hence
[y,x] in (R `) /\ ((R ~) `)
by XBOOLE_0:def 4;
verum
end;
hence
( (R `) /\ ((R ~) `) is irreflexive & (R `) /\ ((R ~) `) is symmetric )
by z1, LemSym, RELAT_2:2; verum