let X be set ; for R being Relation of X st R is symmetric holds
R ` is symmetric
let R be Relation of X; ( R is symmetric implies R ` is symmetric )
assume A1:
R is symmetric
; R ` is symmetric
for x, y being object st [x,y] in R ` holds
[y,x] in R `
proof
let x,
y be
object ;
( [x,y] in R ` implies [y,x] in R ` )
assume Z0:
[x,y] in R `
;
[y,x] in R `
then xx:
(
x in field (R `) &
y in field (R `) )
by RELAT_1:15;
R /\ (R `) = {}
by XBOOLE_0:def 7, SUBSET_1:23;
then Z1:
( not
[x,y] in R or not
[x,y] in R ` )
by XBOOLE_0:def 4;
assume
not
[y,x] in R `
;
contradiction
then
[y,x] in R
by Lemma12b, xx;
hence
contradiction
by Z0, Z1, LemSym, A1;
verum
end;
hence
R ` is symmetric
by LemSym; verum