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