let p, q, r, s, t be Point of (TOP-REAL 3); ((|{p,q,r}| * |{p,s,t}|) - (|{p,q,s}| * |{p,r,t}|)) + (|{p,q,t}| * |{p,r,s}|) = 0
A1:
|{p,q,r}| = (((((((p `1) * (q `2)) * (r `3)) - (((p `3) * (q `2)) * (r `1))) - (((p `1) * (q `3)) * (r `2))) + (((p `2) * (q `3)) * (r `1))) - (((p `2) * (q `1)) * (r `3))) + (((p `3) * (q `1)) * (r `2))
by Th23;
A2:
|{p,s,t}| = (((((((p `1) * (s `2)) * (t `3)) - (((p `3) * (s `2)) * (t `1))) - (((p `1) * (s `3)) * (t `2))) + (((p `2) * (s `3)) * (t `1))) - (((p `2) * (s `1)) * (t `3))) + (((p `3) * (s `1)) * (t `2))
by Th23;
A3:
|{p,q,s}| = (((((((p `1) * (q `2)) * (s `3)) - (((p `3) * (q `2)) * (s `1))) - (((p `1) * (q `3)) * (s `2))) + (((p `2) * (q `3)) * (s `1))) - (((p `2) * (q `1)) * (s `3))) + (((p `3) * (q `1)) * (s `2))
by Th23;
A4:
|{p,r,t}| = (((((((p `1) * (r `2)) * (t `3)) - (((p `3) * (r `2)) * (t `1))) - (((p `1) * (r `3)) * (t `2))) + (((p `2) * (r `3)) * (t `1))) - (((p `2) * (r `1)) * (t `3))) + (((p `3) * (r `1)) * (t `2))
by Th23;
A5:
|{p,q,t}| = (((((((p `1) * (q `2)) * (t `3)) - (((p `3) * (q `2)) * (t `1))) - (((p `1) * (q `3)) * (t `2))) + (((p `2) * (q `3)) * (t `1))) - (((p `2) * (q `1)) * (t `3))) + (((p `3) * (q `1)) * (t `2))
by Th23;
|{p,r,s}| = (((((((p `1) * (r `2)) * (s `3)) - (((p `3) * (r `2)) * (s `1))) - (((p `1) * (r `3)) * (s `2))) + (((p `2) * (r `3)) * (s `1))) - (((p `2) * (r `1)) * (s `3))) + (((p `3) * (r `1)) * (s `2))
by Th23;
hence
((|{p,q,r}| * |{p,s,t}|) - (|{p,q,s}| * |{p,r,t}|)) + (|{p,q,t}| * |{p,r,s}|) = 0
by A1, A2, A3, A4, A5; verum