for p, q being Point of (TOP-REAL 3) st not p is zero & not q is zero & p <X> q = 0. (TOP-REAL 3) holds
are_Prop p,q