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 A1: ( B is_a_component_of (L~ (SpStSeq D)) ` & not B is Bounded ) ; :: thesis: B = LeftComp (SpStSeq D)
A2: LeftComp (SpStSeq D) is_a_component_of (L~ (SpStSeq D)) ` by GOBOARD9:def 1;
A3: not LeftComp (SpStSeq D) is Bounded by Th98;
consider B1 being Subset of ((TOP-REAL 2) | ((L~ (SpStSeq D)) ` )) such that
A4: ( B1 = B & B1 is_a_component_of (TOP-REAL 2) | ((L~ (SpStSeq D)) ` ) ) by A1, CONNSP_1:def 6;
consider L1 being Subset of ((TOP-REAL 2) | ((L~ (SpStSeq D)) ` )) such that
A5: ( L1 = LeftComp (SpStSeq D) & L1 is_a_component_of (TOP-REAL 2) | ((L~ (SpStSeq D)) ` ) ) by A2, CONNSP_1:def 6;
consider r1 being Real such that
A6: for q being Point of (TOP-REAL 2) st q in L~ (SpStSeq D) holds
|.q.| < r1 by Th40;
reconsider P = (REAL 2) \ { q where q is Point of (TOP-REAL 2) : |.q.| < r1 } as Subset of (TOP-REAL 2) by EUCLID:25;
P c= the carrier of (TOP-REAL 2) \ (L~ (SpStSeq D))

proof

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

now

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

end;

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

end;

then A10: P /\ (the carrier of (TOP-REAL 2) \ (L~ (SpStSeq D))) = P by XBOOLE_1:28;
then A11: Down P,((L~ (SpStSeq D)) ` ) is connected by Th15, Th61;
consider q3 being Point of (TOP-REAL 2) such that
A12: ( q3 in LeftComp (SpStSeq D) & |.q3.| >= r1 ) by A3, Th40;
q3 in the carrier of (TOP-REAL 2) ;
then A13: q3 in REAL 2 by EUCLID:25;

now

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 A12; :: thesis: verum

end;

then q3 in P by A13, XBOOLE_0:def 5;
then A14: L1 meets P by A5, A12, XBOOLE_0:3;
consider q4 being Point of (TOP-REAL 2) such that
A15: ( q4 in B & |.q4.| >= r1 ) by A1, Th40;
q4 in the carrier of (TOP-REAL 2) ;
then A16: q4 in REAL 2 by EUCLID:25;

now

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 A15; :: thesis: verum

end;

then q4 in P by A16, XBOOLE_0:def 5;
then B meets P by A15, XBOOLE_0:3;
hence B = LeftComp (SpStSeq D) by A4, A5, A10, A11, A14, Th100; :: thesis: verum