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