theorem Th33: :: BKMODEL2:43

for h being Element of EnsHomography3 st h = homography (1. (F_Real,3)) holds
h is_K-isometry