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