:: deftheorem defines EnsK-isometry BKMODEL2:def 7 :
EnsK-isometry = { h where h is Element of EnsHomography3 : h is_K-isometry } ;