let p, q be Point of (TOP-REAL 3); |((p <X> q),(p <X> q))| = (|(q,q)| * |(p,p)|) - (|(q,p)| * |(p,q)|)
set r1 = (p <X> q) `1 ;
set r2 = (p <X> q) `2 ;
set r3 = (p <X> q) `3 ;
p <X> q = |[(((p `2) * (q `3)) - ((p `3) * (q `2))),(((p `3) * (q `1)) - ((p `1) * (q `3))),(((p `1) * (q `2)) - ((p `2) * (q `1)))]|
by EUCLID_5:def 4;
then A1:
( (p <X> q) `1 = ((p `2) * (q `3)) - ((p `3) * (q `2)) & (p <X> q) `2 = ((p `3) * (q `1)) - ((p `1) * (q `3)) & (p <X> q) `3 = ((p `1) * (q `2)) - ((p `2) * (q `1)) )
by EUCLID_5:2;
A2:
|((p <X> q),(p <X> q))| = ((((p <X> q) `1) * ((p <X> q) `1)) + (((p <X> q) `2) * ((p <X> q) `2))) + (((p <X> q) `3) * ((p <X> q) `3))
by EUCLID_5:29;
(|(q,q)| * |(p,p)|) - (|(q,p)| * |(p,q)|) =
(((((q `1) * (q `1)) + ((q `2) * (q `2))) + ((q `3) * (q `3))) * |(p,p)|) - (|(q,p)| * |(p,q)|)
by EUCLID_5:29
.=
(((((q `1) * (q `1)) + ((q `2) * (q `2))) + ((q `3) * (q `3))) * ((((p `1) * (p `1)) + ((p `2) * (p `2))) + ((p `3) * (p `3)))) - (|(q,p)| * |(p,q)|)
by EUCLID_5:29
.=
(((((q `1) * (q `1)) + ((q `2) * (q `2))) + ((q `3) * (q `3))) * ((((p `1) * (p `1)) + ((p `2) * (p `2))) + ((p `3) * (p `3)))) - (((((q `1) * (p `1)) + ((q `2) * (p `2))) + ((q `3) * (p `3))) * |(p,q)|)
by EUCLID_5:29
.=
(((((q `1) * (q `1)) + ((q `2) * (q `2))) + ((q `3) * (q `3))) * ((((p `1) * (p `1)) + ((p `2) * (p `2))) + ((p `3) * (p `3)))) - (((((q `1) * (p `1)) + ((q `2) * (p `2))) + ((q `3) * (p `3))) * ((((p `1) * (q `1)) + ((p `2) * (q `2))) + ((p `3) * (q `3))))
by EUCLID_5:29
;
hence
|((p <X> q),(p <X> q))| = (|(q,q)| * |(p,p)|) - (|(q,p)| * |(p,q)|)
by A1, A2; verum