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 <> p1 holds
p1,q split P
let p1, p2, q be Point of (TOP-REAL 2); :: thesis: ( p1,p2 split P & q in P & q <> p1 implies p1,q split P )
assume p1 <> p2 ; :: according to SPPOL_2:def 1 :: thesis: ( for f1, f2 being S-Sequence_in_R2 holds
( not p1 = f1 /. 1 or not p1 = f2 /. 1 or not p2 = f1 /. (len f1) or not p2 = f2 /. (len f2) or not (L~ f1) /\ (L~ f2) = {p1,p2} or not P = (L~ f1) \/ (L~ f2) ) or not q in P or not q <> p1 or p1,q split P )
given f1, f2 being S-Sequence_in_R2 such that A1: p1 = f1 /. 1 and
A2: p1 = f2 /. 1 and
A3: p2 = f1 /. (len f1) and
A4: p2 = f2 /. (len f2) and
A5: (L~ f1) /\ (L~ f2) = {p1,p2} and
A6: P = (L~ f1) \/ (L~ f2) ; :: thesis: ( not q in P or not q <> p1 or p1,q split P )
assume A7: q in P ; :: thesis: ( not q <> p1 or p1,q split P )
assume A8: q <> p1 ; :: thesis: p1,q split P
hence p1 <> q ; :: according to SPPOL_2:def 1 :: thesis: ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) )

per cases ( q in L~ f1 or q in L~ f2 ) by A6, A7, XBOOLE_0:def 3;

suppose A9: q in L~ f1 ; :: thesis: ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) )

now

per cases ( q in rng f1 or not q in rng f1 ) ;

suppose q in rng f1 ; :: thesis: ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) )

hence ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) ) by A1, A2, A3, A4, A5, A6, A8, Lm16; :: thesis: verum

end;

suppose A10: not q in rng f1 ; :: thesis: ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) )

consider i being Element of NAT such that
A11: 1 <= i and
A12: i + 1 <= len f1 and
A13: q in LSeg (f1,i) by A9, Th13;
reconsider f19 = Ins (f1,i,q) as S-Sequence_in_R2 by A10, A13, Th52;
A14: L~ f19 = L~ f1 by A13, Th26;
len f19 = (len f1) + 1 by FINSEQ_5:69;
then A15: p2 = f19 /. (len f19) by A3, A12, FINSEQ_5:74;
A16: q in rng f19 by FINSEQ_5:71;
p1 = f19 /. 1 by A1, A11, FINSEQ_5:75;
hence ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) ) by A2, A4, A5, A6, A8, A16, A15, A14, Lm16; :: thesis: verum

end;

end;

end;

hence ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) ) ; :: thesis: verum

end;

suppose A17: q in L~ f2 ; :: thesis: ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) )

now

per cases ( q in rng f2 or not q in rng f2 ) ;

suppose q in rng f2 ; :: thesis: ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) )

hence ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) ) by A1, A2, A3, A4, A5, A6, A8, Lm16; :: thesis: verum

end;

suppose A18: not q in rng f2 ; :: thesis: ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) )

consider i being Element of NAT such that
A19: 1 <= i and
A20: i + 1 <= len f2 and
A21: q in LSeg (f2,i) by A17, Th13;
reconsider f29 = Ins (f2,i,q) as S-Sequence_in_R2 by A18, A21, Th52;
A22: L~ f29 = L~ f2 by A21, Th26;
len f29 = (len f2) + 1 by FINSEQ_5:69;
then A23: p2 = f29 /. (len f29) by A4, A20, FINSEQ_5:74;
A24: q in rng f29 by FINSEQ_5:71;
p1 = f29 /. 1 by A2, A19, FINSEQ_5:75;
hence ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) ) by A1, A3, A5, A6, A8, A24, A23, A22, Lm16; :: thesis: verum

end;

end;

end;

hence ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) ) ; :: thesis: verum

end;

end;