let p, q be Point of (TOP-REAL 3); :: thesis: |(p,(p <X> q))| = 0
thus |(p,(p <X> q))| = |{p,p,q}| by EUCLID_5:def 5
.= 0 by EUCLID_5:31 ; :: thesis: verum