let p, q be Point of (TOP-REAL 3); |{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)|)
; verum