theorem Th128: :: MATGRP_0:110

for R being Ring
for n being Nat
for X being Matrix of n,R holds
( X is Element of (GL (n,R)) iff X is invertible ) by Th126;