let R be Relation; :: thesis: ( R is symmetric iff R = R ~ )

hereby :: thesis: ( R = R ~ implies R is symmetric )

assume R is symmetric ; :: thesis: R = R ~
then A2: R is_symmetric_in field R by Def11;

now :: thesis: for a, b being set holds
( [a,b] in R iff [a,b] in R ~ )

let a, b be set ; :: thesis: ( [a,b] in R iff [a,b] in R ~ )

A3: now :: thesis: ( [a,b] in R ~ implies [a,b] in R )

assume [a,b] in R ~ ; :: thesis: [a,b] in R
then A4: [b,a] in R by RELAT_1:def 7;
then ( a in field R & b in field R ) by RELAT_1:15;
hence [a,b] in R by A2, A4, Def3; :: thesis: verum

end;

now :: thesis: ( [a,b] in R implies [a,b] in R ~ )

assume A5: [a,b] in R ; :: thesis: [a,b] in R ~
then ( a in field R & b in field R ) by RELAT_1:15;
then [b,a] in R by A2, A5, Def3;
hence [a,b] in R ~ by RELAT_1:def 7; :: thesis: verum

end;

hence ( [a,b] in R iff [a,b] in R ~ ) by A3; :: thesis: verum

end;

hence R = R ~ by RELAT_1:def 2; :: thesis: verum

end;

assume R = R ~ ; :: thesis: R is symmetric
then for a, b being set st a in field R & b in field R & [a,b] in R holds
[b,a] in R by RELAT_1:def 7;
hence R is symmetric by Def3, Def11; :: thesis: verum