let p, q be Point of (TOP-REAL 3); :: thesis: |{p,q,(p <X> q)}| = |.(p <X> q).| ^2
|{p,q,(p <X> q)}| = (|(q,q)| * |(p,p)|) - (|(q,p)| * |(p,q)|) by Th45
.= |((p <X> q),(p <X> q))| by Th46 ;
hence |{p,q,(p <X> q)}| = |.(p <X> q).| ^2 by EUCLID_2:4; :: thesis: verum