:: deftheorem defines is_K-isometry BKMODEL2:def 6 :
for h being Element of EnsHomography3 holds
( h is_K-isometry iff ex N being invertible Matrix of 3,F_Real st
( h = homography N & (homography N) .: absolute = absolute ) );