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