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