let D be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( RightComp (SpStSeq D) c= BDD (L~ (SpStSeq D)) & RightComp (SpStSeq D) is bounded )
set f = SpStSeq D;
set A = L~ (SpStSeq D);
A1: RightComp (SpStSeq D) is_a_component_of (L~ (SpStSeq D)) ` by GOBOARD9:def 2;

A2: now :: thesis: RightComp (SpStSeq D) is bounded

A3: LeftComp (SpStSeq D) misses RightComp (SpStSeq D) by SPRECT_1:88;
assume not RightComp (SpStSeq D) is bounded ; :: thesis: contradiction
hence contradiction by A1, A3, Th77; :: thesis: verum

end;

then A4: RightComp (SpStSeq D) is_inside_component_of L~ (SpStSeq D) by A1;
RightComp (SpStSeq D) c= union { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of L~ (SpStSeq D) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in RightComp (SpStSeq D) or x in union { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of L~ (SpStSeq D) } )
assume A5: x in RightComp (SpStSeq D) ; :: thesis: x in union { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of L~ (SpStSeq D) }
RightComp (SpStSeq D) in { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of L~ (SpStSeq D) } by A4;
hence x in union { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of L~ (SpStSeq D) } by A5, TARSKI:def 4; :: thesis: verum

end;

hence RightComp (SpStSeq D) c= BDD (L~ (SpStSeq D)) ; :: thesis: RightComp (SpStSeq D) is bounded
thus RightComp (SpStSeq D) is bounded by A2; :: thesis: verum