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

A1: now

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

now

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

A3: now

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:30;
hence [a,b] in R by A2, A4, Def3; :: thesis: verum

end;

now

assume A5: [a,b] in R ; :: thesis: [a,b] in R ~
then ( a in field R & b in field R ) by RELAT_1:30;
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;

now

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;
then R is_symmetric_in field R by Def3;
hence R is symmetric by Def11; :: thesis: verum

end;

hence ( R is symmetric iff R = R ~ ) by A1; :: thesis: verum