:: deftheorem Def05 defines SubGroupK-isometry BKMODEL2:def 8 :
for b₁ being strict Subgroup of GroupHomography3 holds
( b₁ = SubGroupK-isometry iff the carrier of b₁ = EnsK-isometry );