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;
per cases ( p1 = q1 or p1 = q2 or p1 <> q1 or p2 <> q1 ) ;
suppose p1 = q1 ; :: thesis: q1,q2 split P
hence q1,q2 split P by A1, A3, A4, Th51; :: thesis: verum
end;
suppose p1 = q2 ; :: thesis: q1,q2 split P
hence q1,q2 split P by A2, A4, A5, Th52; :: thesis: verum
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;
suppose p2 <> q1 ; :: thesis: q1,q2 split P
then q1,p2 split P by A1, A2, Th52;
hence q1,q2 split P by A3, A4, Th51; :: thesis: verum
end;
end;