let X be set ; :: thesis: for R being Relation of X st R is symmetric holds
R ` is symmetric
let R be Relation of X; :: thesis: ( R is symmetric implies R ` is symmetric )
assume A1: R is symmetric ; :: thesis: R ` is symmetric
for x, y being object st [x,y] in R ` holds
[y,x] in R `
proof
let x, y be object ; :: thesis: ( [x,y] in R ` implies [y,x] in R ` )
assume Z0: [x,y] in R ` ; :: thesis: [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 ` ; :: thesis: contradiction
then [y,x] in R by Lemma12b, xx;
hence contradiction by Z0, Z1, LemSym, A1; :: thesis: verum
end;
hence R ` is symmetric by LemSym; :: thesis: verum