let X be non empty set ; :: thesis: for R being RMembership_Func of X,X holds max (R,(converse R)) is symmetric
let R be RMembership_Func of X,X; :: thesis: max (R,(converse R)) is symmetric
set S = max (R,(converse R));
let x, y be Element of X; :: according to LFUZZY_1:def 5 :: thesis: (max (R,(converse R))) . (x,y) = (max (R,(converse R))) . (y,x)
thus (max (R,(converse R))) . (x,y) = (max (R,(converse R))) . [x,y]
.= max ((R . (x,y)),((converse R) . (x,y))) by FUZZY_1:def 4
.= max ((R . (x,y)),(R . (y,x))) by FUZZY_4:26
.= max (((converse R) . (y,x)),(R . (y,x))) by FUZZY_4:26
.= (max (R,(converse R))) . [y,x] by FUZZY_1:def 4
.= (max (R,(converse R))) . (y,x) ; :: thesis: verum