let n be Element of NAT ; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD C misses LeftComp (Cage C,n)
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: BDD C misses LeftComp (Cage C,n)
set f = Cage C,n;
assume (BDD C) /\ (LeftComp (Cage C,n)) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider x being Point of (TOP-REAL 2) such that
A1: x in (BDD C) /\ (LeftComp (Cage C,n)) by SUBSET_1:10;
BDD C misses UBD C by JORDAN2C:28;
then A2: (BDD C) /\ (UBD C) = {} by XBOOLE_0:def 7;
x in BDD C by A1, XBOOLE_0:def 4;
then not x in UBD C by A2, XBOOLE_0:def 4;
then A3: not x in union (UBD-Family C) by Th14;
A4: x in LeftComp (Cage C,n) by A1, XBOOLE_0:def 4;
UBD (L~ (Cage C,n)) in { (UBD (L~ (Cage C,k))) where k is Element of NAT : verum } ;
then not x in UBD (L~ (Cage C,n)) by A3, TARSKI:def 4;
hence contradiction by A4, GOBRD14:46; :: thesis: verum