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

proof

thus ( R is symmetric implies for x, y being Element of X holds R . (x,y) = R . (y,x) ) by FUZZY_4:26; :: thesis: ( ( for x, y being Element of X holds R . (x,y) = R . (y,x) ) implies R is symmetric )
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 object st [x,y] in dom R holds
(converse R) . (x,y) = R . (x,y)

proof

let x, y be object ; :: 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:87;
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:20;
hence R is symmetric ; :: thesis: verum

end;