let R be commutative Ring; :: thesis: for r, r1 being Element of R st r1 in Unit_Set R holds
ex r2 being Element of R st r1 * r2 = 1. R
let r, r1 be Element of R; :: thesis: ( r1 in Unit_Set R implies ex r2 being Element of R st r1 * r2 = 1. R )
assume A1: r1 in Unit_Set R ; :: thesis: ex r2 being Element of R st r1 * r2 = 1. R
r1 in { a where a is Element of R : a is Unit of R } by A1, RINGFRAC:def 5;
then consider r being Element of [#] R such that
A2: ( r1 = r & r is Unit of R ) ;
reconsider r1 = r1 as Element of R ;
{r1} -Ideal = [#] R by A2, RING_2:20;
then A3: 1. R in {r1} -Ideal ;
{r1} -Ideal = { (r1 * r) where r is Element of R : verum } by IDEAL_1:64;
hence ex r2 being Element of R st r1 * r2 = 1. R by A3; :: thesis: verum