let n be Element of NAT ; :: thesis: for P being connected Subset of (TOP-REAL n)
for Q being Subset of (TOP-REAL n) holds
( not P misses Q or P c= UBD Q or P c= BDD Q )
let P be connected Subset of (TOP-REAL n); :: thesis: for Q being Subset of (TOP-REAL n) holds
( not P misses Q or P c= UBD Q or P c= BDD Q )
let Q be Subset of (TOP-REAL n); :: thesis: ( not P misses Q or P c= UBD Q or P c= BDD Q )
assume A1: P misses Q ; :: thesis: ( P c= UBD Q or P c= BDD Q )

per cases ( P is empty or Q = [#] (TOP-REAL n) or ( not P is empty & Q <> [#] (TOP-REAL n) ) ) ;

suppose P is empty ; :: thesis: ( P c= UBD Q or P c= BDD Q )

hence ( P c= UBD Q or P c= BDD Q ) by XBOOLE_1:2; :: thesis: verum

end;

suppose Q = [#] (TOP-REAL n) ; :: thesis: ( P c= UBD Q or P c= BDD Q )

then P = {} by A1, XBOOLE_1:67;
hence ( P c= UBD Q or P c= BDD Q ) by XBOOLE_1:2; :: thesis: verum

end;

suppose that A2: not P is empty and
A3: Q <> [#] (TOP-REAL n) ; :: thesis: ( P c= UBD Q or P c= BDD Q )

(Q `) ` <> [#] (TOP-REAL n) by A3;
then A4: Q ` <> {} (TOP-REAL n) ;
P c= Q ` by A1, SUBSET_1:23;
then consider C being Subset of (TOP-REAL n) such that
A5: C is_a_component_of Q ` and
A6: P c= C by A2, A4, GOBOARD9:3;
( C is_inside_component_of Q or C is_outside_component_of Q ) by A5, Th14;
then ( C c= UBD Q or C c= BDD Q ) by JORDAN2C:22, JORDAN2C:23;
hence ( P c= UBD Q or P c= BDD Q ) by A6, XBOOLE_1:1; :: thesis: verum

end;

end;