let D be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: LeftComp (SpStSeq D) c= UBD (L~ (SpStSeq D))
set f = SpStSeq D;
set A = L~ (SpStSeq D);
( LeftComp (SpStSeq D) is_a_component_of (L~ (SpStSeq D)) ` & not LeftComp (SpStSeq D) is bounded ) by Th74, GOBOARD9:def 1;
then A1: LeftComp (SpStSeq D) is_outside_component_of L~ (SpStSeq D) ;
LeftComp (SpStSeq D) c= union { B where B is Subset of (TOP-REAL 2) : B is_outside_component_of L~ (SpStSeq D) }

proof

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

end;

hence LeftComp (SpStSeq D) c= UBD (L~ (SpStSeq D)) ; :: thesis: verum