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

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

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

assume
R = R ~
; :: thesis: R is symmetric assume
R is symmetric
; :: thesis: R = R ~

then A1: R is_symmetric_in field R ;

end;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 ~ )

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

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

end;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;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

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

hence
( [a,b] in R iff [a,b] in R ~ )
by A2; :: thesis: verumassume 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;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

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