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