theorem Th17: :: MATRIX_6:16

for R being Ring
for n being Nat
for M being Matrix of n,R st M is invertible holds
( M ~ is invertible & (M ~) ~ = M )