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)

then converse R = R by A2, BINOP_1:20;

hence R is symmetric ; :: 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 object st [x,y] in dom R holds

(converse R) . (x,y) = R . (x,y)

proof

( dom (converse R) = [:X,X:] & dom R = [:X,X:] )
by FUNCT_2:def 1;
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;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

then converse R = R by A2, BINOP_1:20;

hence R is symmetric ; :: thesis: verum