let X be non empty set ; :: thesis: 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; :: thesis: ( (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 ; :: thesis: ( [x,y] in (R `) /\ ((R ~) `) implies [y,x] in (R `) /\ ((R ~) `) )
assume B0: [x,y] in (R `) /\ ((R ~) `) ; :: thesis: [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; :: thesis: verum

end;

hence ( (R `) /\ ((R ~) `) is irreflexive & (R `) /\ ((R ~) `) is symmetric ) by z1, LemSym, RELAT_2:2; :: thesis: verum