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 5
.= 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 5
.= (max R,(converse R)) . y,x ; :: thesis: verum