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 (min R,S) = min R,S
let R, S be RMembership_Func of X,X; :: thesis: ( R is symmetric & S is symmetric implies converse (min R,S) = min R,S )
assume ( R is symmetric & S is symmetric ) ; :: thesis: converse (min R,S) = min R,S
then ( converse R = R & converse S = S ) by Def4;
hence converse (min R,S) = min R,S by FUZZY_4:8; :: thesis: verum