let f be FinSequence of (TOP-REAL 2); :: thesis: for q being Point of (TOP-REAL 2) st q in rng f & 1 <> q .. f & q .. f <> len f & f is unfolded & f is s.n.c. holds
(L~ (f -: q)) /\ (L~ (f :- q)) = {q}
let q be Point of (TOP-REAL 2); :: thesis: ( q in rng f & 1 <> q .. f & q .. f <> len f & f is unfolded & f is s.n.c. implies (L~ (f -: q)) /\ (L~ (f :- q)) = {q} )
assume that
A1: q in rng f and
A2: 1 <> q .. f and
A3: q .. f <> len f and
A4: f is unfolded and
A5: f is s.n.c. ; :: thesis: (L~ (f -: q)) /\ (L~ (f :- q)) = {q}
A6: (f :- q) /. 1 = q by FINSEQ_5:53;
q .. f <= len f by A1, FINSEQ_4:21;
then q .. f < len f by A3, XXREAL_0:1;
then (q .. f) + 1 <= len f by NAT_1:13;
then A7: 1 <= (len f) - (q .. f) by XREAL_1:19;
len (f :- q) = ((len f) - (q .. f)) + 1 by A1, FINSEQ_5:50;
then 1 + 1 <= len (f :- q) by A7, XREAL_1:6;
then A8: rng (f :- q) c= L~ (f :- q) by Th18;
1 in dom (f :- q) by FINSEQ_5:6;
then A9: q in rng (f :- q) by A6, PARTFUN2:2;
not f -: q is empty by A1, FINSEQ_5:47;
then A10: len (f -: q) in dom (f -: q) by FINSEQ_5:6;
A11: len (f -: q) = q .. f by A1, FINSEQ_5:42;
thus (L~ (f -: q)) /\ (L~ (f :- q)) c= {q} :: according to XBOOLE_0:def 10 :: thesis: {q} c= (L~ (f -: q)) /\ (L~ (f :- q))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (L~ (f -: q)) /\ (L~ (f :- q)) or x in {q} )
assume A12: x in (L~ (f -: q)) /\ (L~ (f :- q)) ; :: thesis: x in {q}
then reconsider p = x as Point of (TOP-REAL 2) ;
p in L~ (f -: q) by A12, XBOOLE_0:def 4;
then consider i being Nat such that
A13: 1 <= i and
A14: i + 1 <= len (f -: q) and
A15: p in LSeg ((f -: q),i) by Th13;
A16: LSeg ((f -: q),i) = LSeg (f,i) by A14, Th9;
p in L~ (f :- q) by A12, XBOOLE_0:def 4;
then consider j being Nat such that
A17: 1 <= j and
j + 1 <= len (f :- q) and
A18: p in LSeg ((f :- q),j) by Th13;
consider j9 being Nat such that
A19: j = j9 + 1 by A17, NAT_1:6;
reconsider j9 = j9 as Element of NAT by ORDINAL1:def 12;
A20: LSeg ((f :- q),j) = LSeg (f,(j9 + (q .. f))) by A1, A19, Th10;

per cases ( ( i + 1 = len (f -: q) & j9 = 0 ) or ( i + 1 = len (f -: q) & j9 <> 0 ) or i + 1 <> len (f -: q) ) ;

suppose that A21: i + 1 = len (f -: q) and
A22: j9 = 0 ; :: thesis: x in {q}

q .. f <= len f by A1, FINSEQ_4:21;
then q .. f < len f by A3, XXREAL_0:1;
then (i + 1) + 1 <= len f by A11, A21, NAT_1:13;
then i + (1 + 1) <= len f ;
then (LSeg ((f -: q),i)) /\ (LSeg ((f :- q),j)) = {(f /. (q .. f))} by A4, A11, A13, A16, A20, A21, A22
.= {q} by A1, FINSEQ_5:38 ;
hence x in {q} by A15, A18, XBOOLE_0:def 4; :: thesis: verum

end;

suppose that A23: i + 1 = len (f -: q) and
A24: j9 <> 0 ; :: thesis: x in {q}

1 <= j9 by A24, NAT_1:14;
then (i + 1) + 1 <= j9 + (q .. f) by A11, A23, XREAL_1:7;
then i + 1 < j9 + (q .. f) by NAT_1:13;
then LSeg ((f -: q),i) misses LSeg ((f :- q),j) by A5, A16, A20;
then (LSeg ((f -: q),i)) /\ (LSeg ((f :- q),j)) = {} ;
hence x in {q} by A15, A18, XBOOLE_0:def 4; :: thesis: verum

end;

suppose A25: i + 1 <> len (f -: q) ; :: thesis: x in {q}

A26: q .. f <= j9 + (q .. f) by NAT_1:11;
i + 1 < q .. f by A11, A14, A25, XXREAL_0:1;
then i + 1 < j9 + (q .. f) by A26, XXREAL_0:2;
then LSeg ((f -: q),i) misses LSeg ((f :- q),j) by A5, A16, A20;
then (LSeg ((f -: q),i)) /\ (LSeg ((f :- q),j)) = {} ;
hence x in {q} by A15, A18, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

1 <= q .. f by A1, FINSEQ_4:21;
then 1 < q .. f by A2, XXREAL_0:1;
then 1 + 1 <= q .. f by NAT_1:13;
then A27: rng (f -: q) c= L~ (f -: q) by A11, Th18;
(f -: q) /. (q .. f) = q by A1, FINSEQ_5:45;
then q in rng (f -: q) by A11, A10, PARTFUN2:2;
then q in (L~ (f -: q)) /\ (L~ (f :- q)) by A27, A9, A8, XBOOLE_0:def 4;
hence {q} c= (L~ (f -: q)) /\ (L~ (f :- q)) by ZFMISC_1:31; :: thesis: verum