let o, p, q, r be Point of (TOP-REAL 3); :: thesis: ( |{o,p,((o <X> p) <X> (q <X> r))}| = 0 & |{q,r,((o <X> p) <X> (q <X> r))}| = 0 )
set s = (o <X> p) <X> (q <X> r);
thus |{o,p,((o <X> p) <X> (q <X> r))}| = |((o <X> p),((o <X> p) <X> (q <X> r)))| by EUCLID_5:35
.= 0 by Th38 ; :: thesis: |{q,r,((o <X> p) <X> (q <X> r))}| = 0
thus |{q,r,((o <X> p) <X> (q <X> r))}| = |((q <X> r),((o <X> p) <X> (q <X> r)))| by EUCLID_5:35
.= 0 by Th39 ; :: thesis: verum