theorem :: BKMODEL4:56

for P, Q being non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) st P in absolute & Q in absolute holds
RP3_to_T2 Dir001, RP3_to_T2 P equiv RP3_to_T2 Dir001, RP3_to_T2 Q