homography (1. (F_Real,3)) in EnsHomography3 ;
hence not EnsHomography3 is empty ; :: thesis: verum