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 ) by A1, RELAT_2:def 3;
A3: ( x in field r & y in field r & [y,x] in r implies [x,y] in r ) by A1, RELAT_2:def 3;