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

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