theorem Th46: :: ANPROJ_8:54

for p, q being Point of (TOP-REAL 3) holds |((p <X> q),(p <X> q))| = (|(q,q)| * |(p,p)|) - (|(q,p)| * |(p,q)|)