let p, q be Point of (TOP-REAL 3); :: thesis: |{p,q,(p <X> q)}| = (|(q,q)| * |(p,p)|) - (|(q,p)| * |(p,q)|)
|{p,q,(p <X> q)}| = |(p,(q <X> (p <X> q)))| by EUCLID_5:def 5
.= |(p,((|(q,q)| * p) - (|(q,p)| * q)))| by EUCLID_5:32
.= |(p,(|(q,q)| * p))| - |(p,(|(q,p)| * q))| by EUCLID_2:27
.= (|(q,q)| * |(p,p)|) - |(p,(|(q,p)| * q))| by EUCLID_2:20
.= (|(q,q)| * |(p,p)|) - (|(q,p)| * |(p,q)|) by EUCLID_2:20 ;
hence |{p,q,(p <X> q)}| = (|(q,q)| * |(p,p)|) - (|(q,p)| * |(p,q)|) ; :: thesis: verum