theorem Th45: :: ANPROJ_8:53
for p, q being Point of (TOP-REAL 3) holds |{p,q,(p <X> q)}| = (|(q,q)| * |(p,p)|) - (|(q,p)| * |(p,q)|)