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 r2 * r1 = 1. R
let r1 be Element of R; :: thesis: ( r1 in Unit_Set R implies ex r2 being Element of R st r2 * r1 = 1. R )
assume r1 in Unit_Set R ; :: thesis: ex r2 being Element of R st r2 * r1 = 1. R
then ex r2 being Element of R st r1 * r2 = 1. R by Th9;
hence ex r2 being Element of R st r2 * r1 = 1. R ; :: thesis: verum