:: deftheorem Def10 defines SubIsomGroupRel VECTMETR:def 10 :
for n being Element of NAT
for G being Subgroup of IsomGroup n
for b₃ being Relation of the carrier of (RLMSpace n) holds
( b₃ = SubIsomGroupRel G iff for A, B being Element of (RLMSpace n) holds
( [A,B] in b₃ iff ex f being Function st
( f in the carrier of G & f . A = B ) ) );