1. R in S by C0SP1:def 4;
then [(1. R),(1. R)] in Frac S by Def3;
hence not Frac S is empty ; :: thesis: verum