theorem Th18: :: BKMODEL3:21

1_ GroupLineHomography3 = line_homography (1. (F_Real,3))