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, Lm17; :: 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 f1' = Ins f1,i,q as S-Sequence_in_R2 by A10, A13, Th52;
A14: q in rng f1' by FINSEQ_5:74;
A15: p1 = f1' /. 1 by A1, A11, FINSEQ_5:78;
len f1' = (len f1) + 1 by FINSEQ_5:72;
then A16: p2 = f1' /. (len f1') by A3, A12, FINSEQ_5:77;
L~ f1' = L~ f1 by A13, Th26;
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, A14, A15, A16, Lm17; :: 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, Lm17; :: 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 f2' = Ins f2,i,q as S-Sequence_in_R2 by A18, A21, Th52;
A22: q in rng f2' by FINSEQ_5:74;
A23: p1 = f2' /. 1 by A2, A19, FINSEQ_5:78;
len f2' = (len f2) + 1 by FINSEQ_5:72;
then A24: p2 = f2' /. (len f2') by A4, A20, FINSEQ_5:77;
L~ f2' = L~ f2 by A21, Th26;
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, A22, A23, A24, Lm17; :: 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;