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