thus ( R is symmetric iff for x, y being Element of X holds R . (x,y) = R . (y,x) ) :: thesis: verum

proof

hereby :: thesis: ( ( for x, y being Element of X holds R . (x,y) = R . (y,x) ) implies R is symmetric )

assume R is symmetric ; :: thesis: for x, y being Element of X holds R . (x,y) = R . (y,x)
then converse R = R by Def4;
hence for x, y being Element of X holds R . (x,y) = R . (y,x) by FUZZY_4:26; :: thesis: verum

end;

assume A1: for x, y being Element of X holds R . (x,y) = R . (y,x) ; :: thesis: R is symmetric
A2: for x, y being set st [x,y] in dom R holds
(converse R) . (x,y) = R . (x,y)

proof

let x, y be set ; :: thesis: ( [x,y] in dom R implies (converse R) . (x,y) = R . (x,y) )
assume [x,y] in dom R ; :: thesis: (converse R) . (x,y) = R . (x,y)
then reconsider x = x, y = y as Element of X by ZFMISC_1:106;
R . (x,y) = R . (y,x) by A1;
hence (converse R) . (x,y) = R . (x,y) by FUZZY_4:26; :: thesis: verum

end;

( dom (converse R) = [:X,X:] & dom R = [:X,X:] ) by FUNCT_2:def 1;
then converse R = R by A2, BINOP_1:32;
hence R is symmetric by Def4; :: thesis: verum

end;