for P being non zero_proj1 non zero_proj2 non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) holds
( dual1 P = dual2 P & dual1 P = dual3 P & dual2 P = dual3 P ) by Th33, Th34, Th35;