let X be set ; :: thesis: for R being Relation st R is symmetric holds
R .: X = R " X
let R be Relation; :: thesis: ( R is symmetric implies R .: X = R " X )
assume A1: R is symmetric ; :: thesis: R .: X = R " X

hereby :: according to XBOOLE_0:def 10,TARSKI:def 3 :: thesis: R " X c= R .: X

let y be object ; :: thesis: ( y in R .: X implies y in R " X )
assume y in R .: X ; :: thesis: y in R " X
then consider z being object such that
A2: [z,y] in R and
A3: z in X by RELAT_1:def 13;
[y,z] in R by A2, A1, Lm3;
hence y in R " X by A3, RELAT_1:def 14; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in R " X or y in R .: X )
assume y in R " X ; :: thesis: y in R .: X
then consider z being object such that
A4: [y,z] in R and
A5: z in X by RELAT_1:def 14;
[z,y] in R by A4, A1, Lm3;
hence y in R .: X by A5, RELAT_1:def 13; :: thesis: verum