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

then converse R = R by A2, BINOP_1:32;
hence R is symmetric by Def4; :: thesis: verum

end;