let n be 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 ) ; :: 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 ) ; :: thesis: verum
end;
suppose that A2: not P is empty and
Q <> [#] (TOP-REAL n) ; :: thesis: ( P c= UBD Q or P c= BDD Q )
P c= Q ` by A1, SUBSET_1:23;
then consider C being Subset of (TOP-REAL n) such that
A3: C is_a_component_of Q ` and
A4: P c= C by A2, GOBOARD9:3;
( C is_inside_component_of Q or C is_outside_component_of Q ) by A3, 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 A4; :: thesis: verum
end;
end;