set r = 1. R;
1. R in Unit_Set R ;
hence not Unit_Set R is empty ; :: thesis: verum