converse (min R,S) = min R,S by Th9;
hence min R,S is symmetric by Def4; :: thesis: verum