:: deftheorem defines Orthogonal MATRIX_6:def 7 :
for n being Nat
for K being Field
for M1 being Matrix of n,K holds
( M1 is Orthogonal iff ( M1 is invertible & M1 @ = M1 ~ ) );