set F = { B where B is Subset of (TOP-REAL 2) : B is_outside_component_of C } ;
{ B where B is Subset of (TOP-REAL 2) : B is_outside_component_of C } c= bool the carrier of (TOP-REAL 2)

proof

let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in { B where B is Subset of (TOP-REAL 2) : B is_outside_component_of C } or f in bool the carrier of (TOP-REAL 2) )
assume f in { B where B is Subset of (TOP-REAL 2) : B is_outside_component_of C } ; :: thesis: f in bool the carrier of (TOP-REAL 2)
then ex B being Subset of (TOP-REAL 2) st
( f = B & B is_outside_component_of C ) ;
hence f in bool the carrier of (TOP-REAL 2) ; :: thesis: verum

end;

then reconsider F = { B where B is Subset of (TOP-REAL 2) : B is_outside_component_of C } as Subset-Family of (TOP-REAL 2) ;
F is open

proof

let P be Subset of (TOP-REAL 2); :: according to TOPS_2:def 1 :: thesis: ( not P in F or P is open )
assume P in F ; :: thesis: P is open
then consider B being Subset of (TOP-REAL 2) such that
A3: P = B and
A4: B is_outside_component_of C ;
B is_a_component_of C ` by A4;
hence P is open by A3, SPRECT_3:8; :: thesis: verum

end;

hence UBD C is open by TOPS_2:19; :: thesis: verum