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 A1: R is_symmetric_in field R ;

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

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

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

assume [a,b] in R ~ ; :: thesis: [a,b] in R
then A3: [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 A1, A3; :: thesis: verum

end;

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

assume A4: [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 A1, A4;
hence [a,b] in R ~ by RELAT_1:def 7; :: thesis: verum

end;

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

end;

hence R = R ~ ; :: thesis: verum

end;

assume R = R ~ ; :: thesis: R is symmetric
then for a, b being object 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; :: thesis: verum