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 and
A3: q <> p2 ; :: thesis: q,p2 split P
p2,p1 split P by A1, Th50;
then p2,q split P by A2, A3, Th51;
hence q,p2 split P by Th50; :: thesis: verum