let P be Subset of (TOP-REAL 2); :: thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) st p1,p2 split P & q1 in P & q2 in P & q1 <> q2 holds

q1,q2 split P

let p1, p2, q1, q2 be Point of (TOP-REAL 2); :: thesis: ( p1,p2 split P & q1 in P & q2 in P & q1 <> q2 implies q1,q2 split P )

assume that

A1: p1,p2 split P and

A2: q1 in P and

A3: q2 in P and

A4: q1 <> q2 ; :: thesis: q1,q2 split P

A5: p2,p1 split P by A1, Th50;

q1,q2 split P

let p1, p2, q1, q2 be Point of (TOP-REAL 2); :: thesis: ( p1,p2 split P & q1 in P & q2 in P & q1 <> q2 implies q1,q2 split P )

assume that

A1: p1,p2 split P and

A2: q1 in P and

A3: q2 in P and

A4: q1 <> q2 ; :: thesis: q1,q2 split P

A5: p2,p1 split P by A1, Th50;

per cases
( p1 = q1 or p1 = q2 or p1 <> q1 or p2 <> q1 )
;

end;

suppose
p1 <> q1
; :: thesis: q1,q2 split P

then
p1,q1 split P
by A1, A2, Th51;

then q2,q1 split P by A3, A4, Th52;

hence q1,q2 split P by Th50; :: thesis: verum

end;then q2,q1 split P by A3, A4, Th52;

hence q1,q2 split P by Th50; :: thesis: verum