Class ((EqRel S),(1. (R,S))) in Class (EqRel S) by EQREL_1:def 3;
hence not S ~ R is empty by Def6; :: thesis: verum