let P be Subset of (TOP-REAL 2); :: thesis: for p1, p2, q being Point of (TOP-REAL 2) st p1,p2 split P & q in P & q <> p2 holds
q,p2 split P
let p1, p2, q be Point of (TOP-REAL 2); :: thesis: ( p1,p2 split P & q in P & q <> p2 implies q,p2 split P )
assume that
A1: p1,p2 split P and
A2: ( q in P & q <> p2 ) ; :: thesis: q,p2 split P
p2,p1 split P by A1, Th54;
then p2,q split P by A2, Th55;
hence q,p2 split P by Th54; :: thesis: verum