let D be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for B being Subset of (TOP-REAL 2) st B is_a_component_of (L~ (SpStSeq D)) ` & not B is bounded holds
B = LeftComp (SpStSeq D)
let B be Subset of (TOP-REAL 2); :: thesis: ( B is_a_component_of (L~ (SpStSeq D)) ` & not B is bounded implies B = LeftComp (SpStSeq D) )
set f = SpStSeq D;
assume that
A1: B is_a_component_of (L~ (SpStSeq D)) ` and
A2: not B is bounded ; :: thesis: B = LeftComp (SpStSeq D)
A3: ex B1 being Subset of ((TOP-REAL 2) | ((L~ (SpStSeq D)) `)) st
( B1 = B & B1 is a_component ) by A1, CONNSP_1:def 6;
consider r1 being Real such that
A4: for q being Point of (TOP-REAL 2) st q in L~ (SpStSeq D) holds
|.q.| < r1 by Th21;
consider q4 being Point of (TOP-REAL 2) such that
A5: q4 in B and
A6: |.q4.| >= r1 by A2, Th21;

A7: now :: thesis: not q4 in { q where q is Point of (TOP-REAL 2) : |.q.| < r1 }

assume q4 in { q where q is Point of (TOP-REAL 2) : |.q.| < r1 } ; :: thesis: contradiction
then ex q being Point of (TOP-REAL 2) st
( q = q4 & |.q.| < r1 ) ;
hence contradiction by A6; :: thesis: verum

end;

reconsider P = (REAL 2) \ { q where q is Point of (TOP-REAL 2) : |.q.| < r1 } as Subset of (TOP-REAL 2) by EUCLID:22;
P c= the carrier of (TOP-REAL 2) \ (L~ (SpStSeq D))

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in P or z in the carrier of (TOP-REAL 2) \ (L~ (SpStSeq D)) )
assume A8: z in P ; :: thesis: z in the carrier of (TOP-REAL 2) \ (L~ (SpStSeq D))

now :: thesis: not z in L~ (SpStSeq D)

assume A9: z in L~ (SpStSeq D) ; :: thesis: contradiction
then reconsider q3 = z as Point of (TOP-REAL 2) ;
A10: not q3 in { q where q is Point of (TOP-REAL 2) : |.q.| < r1 } by A8, XBOOLE_0:def 5;
|.q3.| < r1 by A4, A9;
hence contradiction by A10; :: thesis: verum

end;

hence z in the carrier of (TOP-REAL 2) \ (L~ (SpStSeq D)) by A8, XBOOLE_0:def 5; :: thesis: verum

end;

then A11: P /\ ( the carrier of (TOP-REAL 2) \ (L~ (SpStSeq D))) = P by XBOOLE_1:28;
then A12: Down (P,((L~ (SpStSeq D)) `)) is connected by Th40, CONNSP_1:46;
not LeftComp (SpStSeq D) is bounded by Th74;
then consider q3 being Point of (TOP-REAL 2) such that
A13: q3 in LeftComp (SpStSeq D) and
A14: |.q3.| >= r1 by Th21;

A15: now :: thesis: not q3 in { q where q is Point of (TOP-REAL 2) : |.q.| < r1 }

assume q3 in { q where q is Point of (TOP-REAL 2) : |.q.| < r1 } ; :: thesis: contradiction
then ex q being Point of (TOP-REAL 2) st
( q = q3 & |.q.| < r1 ) ;
hence contradiction by A14; :: thesis: verum

end;

q4 in the carrier of (TOP-REAL 2) ;
then q4 in REAL 2 by EUCLID:22;
then q4 in P by A7, XBOOLE_0:def 5;
then A16: B meets P by A5, XBOOLE_0:3;
LeftComp (SpStSeq D) is_a_component_of (L~ (SpStSeq D)) ` by GOBOARD9:def 1;
then consider L1 being Subset of ((TOP-REAL 2) | ((L~ (SpStSeq D)) `)) such that
A17: L1 = LeftComp (SpStSeq D) and
A18: L1 is a_component by CONNSP_1:def 6;
q3 in the carrier of (TOP-REAL 2) ;
then q3 in REAL 2 by EUCLID:22;
then q3 in P by A15, XBOOLE_0:def 5;
then L1 meets P by A17, A13, XBOOLE_0:3;
hence B = LeftComp (SpStSeq D) by A3, A17, A18, A11, A12, A16, Th76; :: thesis: verum