let D be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( UBD (L~ (SpStSeq D)) <> {} & UBD (L~ (SpStSeq D)) is_outside_component_of L~ (SpStSeq D) & BDD (L~ (SpStSeq D)) <> {} & BDD (L~ (SpStSeq D)) is_inside_component_of L~ (SpStSeq D) )
set f = SpStSeq D;
A1: UBD (L~ (SpStSeq D)) = LeftComp (SpStSeq D) by Th103;
hence UBD (L~ (SpStSeq D)) <> {} ; :: thesis: ( UBD (L~ (SpStSeq D)) is_outside_component_of L~ (SpStSeq D) & BDD (L~ (SpStSeq D)) <> {} & BDD (L~ (SpStSeq D)) is_inside_component_of L~ (SpStSeq D) )
( LeftComp (SpStSeq D) is_a_component_of (L~ (SpStSeq D)) ` & not LeftComp (SpStSeq D) is Bounded ) by Th98, GOBOARD9:def 1;
hence UBD (L~ (SpStSeq D)) is_outside_component_of L~ (SpStSeq D) by A1, Def4; :: thesis: ( BDD (L~ (SpStSeq D)) <> {} & BDD (L~ (SpStSeq D)) is_inside_component_of L~ (SpStSeq D) )
A2: BDD (L~ (SpStSeq D)) = RightComp (SpStSeq D) by Th103;
hence BDD (L~ (SpStSeq D)) <> {} ; :: thesis: BDD (L~ (SpStSeq D)) is_inside_component_of L~ (SpStSeq D)
( RightComp (SpStSeq D) is_a_component_of (L~ (SpStSeq D)) ` & RightComp (SpStSeq D) is Bounded ) by Th102, GOBOARD9:def 2;
hence BDD (L~ (SpStSeq D)) is_inside_component_of L~ (SpStSeq D) by A2, Def3; :: thesis: verum