:: deftheorem defines EnsLineHomography3 BKMODEL3:def 3 :
EnsLineHomography3 = { (line_homography N) where N is invertible Matrix of 3,F_Real : verum } ;