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 :: 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 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 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, Th48;
A14: L~ f19 = L~ f1 by A13, Th25;
1 <= i + 1 by NAT_1:11;
then 1 <= len f1 by A12, XXREAL_0:2;
then Z: ( 1 in dom f1 & len f1 in dom f1 ) by FINSEQ_3:25;
then a3: p2 = f1 . (len f1) by A3, PARTFUN1:def 6;
S2: len f19 = (len f1) + 1 by FINSEQ_5:69;
1 <= (len f1) + 1 by NAT_1:11;
then 1 <= len f19 by S2;
then S1: ( len f19 in dom f19 & 1 in dom f19 ) by FINSEQ_3:25;
A15: p2 = f19 . (len f19) by A12, a3, FINSEQ_5:74, S2
.= f19 /. (len f19) by S1, PARTFUN1:def 6 ;
A16: q in rng f19 by FINSEQ_5:71;
p1 = f1 . 1 by Z, A1, PARTFUN1:def 6;
then p1 = f19 . 1 by A11, FINSEQ_5:75
.= f19 /. 1 by PARTFUN1:def 6, S1 ;
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 :: 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 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 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, Th48;
A22: L~ f29 = L~ f2 by A21, Th25;
1 <= i + 1 by NAT_1:11;
then 1 <= len f2 by A20, XXREAL_0:2;
then Z: ( 1 in dom f2 & len f2 in dom f2 ) by FINSEQ_3:25;
then Sa: p2 = f2 . (len f2) by PARTFUN1:def 6, A4;
Sc: len f29 = (len f2) + 1 by FINSEQ_5:69;
then 1 <= len f29 by NAT_1:11;
then Sd: ( 1 in dom f29 & len f29 in dom f29 ) by FINSEQ_3:25;
A23: p2 = f29 . (len f29) by Sc, Sa, A20, FINSEQ_5:74
.= f29 /. (len f29) by PARTFUN1:def 6, Sd ;
A24: q in rng f29 by FINSEQ_5:71;
p1 = f2 . 1 by PARTFUN1:def 6, A2, Z;
then p1 = f29 . 1 by A19, FINSEQ_5:75
.= f29 /. 1 by Sd, PARTFUN1:def 6 ;
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;