let X be set ; :: thesis: for R being Relation of X st R is_symmetric_in X holds
R ~ is_symmetric_in X
let R be Relation of X; :: thesis: ( R is_symmetric_in X implies R ~ is_symmetric_in X )
assume A1: R is_symmetric_in X ; :: thesis: R ~ is_symmetric_in X
now :: thesis: for x, y being object st x in X & y in X & [x,y] in R ~ holds
[y,x] in R ~
let x, y be object ; :: thesis: ( x in X & y in X & [x,y] in R ~ implies [y,x] in R ~ )
assume that
A2: x in X and
A3: y in X and
A4: [x,y] in R ~ ; :: thesis: [y,x] in R ~
[y,x] in R by A4, RELAT_1:def 7;
then [x,y] in R by A2, A3, A1, RELAT_2:def 3;
hence [y,x] in R ~ by RELAT_1:def 7; :: thesis: verum
end;
hence R ~ is_symmetric_in X by RELAT_2:def 3; :: thesis: verum