let R be commutative Ring; :: thesis: {(1. R)} is multiplicatively-closed
set M = {(1. R)};
for r1, r2 being Element of R st r1 in {(1. R)} & r2 in {(1. R)} holds
r1 * r2 in {(1. R)}

proof

let r1, r2 be Element of R; :: thesis: ( r1 in {(1. R)} & r2 in {(1. R)} implies r1 * r2 in {(1. R)} )
assume A2: ( r1 in {(1. R)} & r2 in {(1. R)} ) ; :: thesis: r1 * r2 in {(1. R)}
then r1 * r2 = (1. R) * r1 by TARSKI:def 1
.= 1. R by A2, TARSKI:def 1 ;
hence r1 * r2 in {(1. R)} by TARSKI:def 1; :: thesis: verum

end;

hence {(1. R)} is multiplicatively-closed by TARSKI:def 1; :: thesis: verum