let X be non empty set ; :: thesis: for r being Relation of X st r is symmetric holds
chi r,[:X,X:] is symmetric
let r be Relation of X; :: thesis: ( r is symmetric implies chi r,[:X,X:] is symmetric )
assume r is symmetric ; :: thesis: chi r,[:X,X:] is symmetric
then A1: r is_symmetric_in field r by RELAT_2:def 11;
let x, y be Element of X; :: according to LFUZZY_1:def 5 :: thesis: (chi r,[:X,X:]) . x,y = (chi r,[:X,X:]) . y,x
A2: ( ( x in field r & y in field r & [x,y] in r implies [y,x] in r ) & ( x in field r & y in field r & [y,x] in r implies [x,y] in r ) ) by A1, RELAT_2:def 3;

per cases ( [x,y] in r or not [x,y] in r ) ;

suppose [x,y] in r ; :: thesis: (chi r,[:X,X:]) . x,y = (chi r,[:X,X:]) . y,x

then ( (chi r,[:X,X:]) . [x,y] = 1 & (chi r,[:X,X:]) . [y,x] = 1 ) by A2, FUNCT_3:def 3, RELAT_1:30;
hence (chi r,[:X,X:]) . x,y = (chi r,[:X,X:]) . y,x ; :: thesis: verum

end;

suppose A3: not [x,y] in r ; :: thesis: (chi r,[:X,X:]) . x,y = (chi r,[:X,X:]) . y,x

then not [y,x] in r by A2, RELAT_1:30;
then ( (chi r,[:X,X:]) . [x,y] = 0 & (chi r,[:X,X:]) . [y,x] = 0 ) by A3, FUNCT_3:def 3;
hence (chi r,[:X,X:]) . x,y = (chi r,[:X,X:]) . y,x ; :: thesis: verum

end;

end;