let X be non empty set ; :: thesis: for R, S being RMembership_Func of X,X st R is symmetric & S is symmetric holds
converse (max (R,S)) = max (R,S)
let R, S be RMembership_Func of X,X; :: thesis: ( R is symmetric & S is symmetric implies converse (max (R,S)) = max (R,S) )
assume ( R is symmetric & S is symmetric ) ; :: thesis: converse (max (R,S)) = max (R,S)
then ( converse R = R & converse S = S ) by Def4;
hence converse (max (R,S)) = max (R,S) by FUZZY_4:7; :: thesis: verum