theorem :: ANPROJ_8:56

for p, q being Point of (TOP-REAL 3) holds |{p,q,(p <X> q)}| = |.(p <X> q).| ^2