let R be commutative Ring; :: thesis: for r1 being Element of R st r1 in Unit_Set R holds
ex r2 being Element of R st r1 * r2 = 1. R
let r1 be Element of R; :: thesis: ( r1 in Unit_Set R implies ex r2 being Element of R st r1 * r2 = 1. R )
assume r1 in Unit_Set R ; :: thesis: ex r2 being Element of R st r1 * r2 = 1. R
then consider r being Element of [#] R such that
A2: r1 = r and
A3: r is Unit of R ;
reconsider r1 = r1 as Element of R ;
{r1} -Ideal = [#] R by A2, A3, RING_2:20;
then A4: 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 A4; :: thesis: verum