:: deftheorem defines EnsHomography3 ANPROJ_9:def 1 :
EnsHomography3 = { (homography N) where N is invertible Matrix of 3,F_Real : verum } ;