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 Th79;
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 Th74, GOBOARD9:def 1;
hence UBD (L~ (SpStSeq D)) is_outside_component_of L~ (SpStSeq D) by A1; :: 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 Th79;
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 Th78, GOBOARD9:def 2;
hence BDD (L~ (SpStSeq D)) is_inside_component_of L~ (SpStSeq D) by A2; :: thesis: verum