let n be 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:4;
BDD C misses UBD C by JORDAN2C:24;
then A2: (BDD C) /\ (UBD C) = {} ;
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 Nat : verum } ;
then not x in UBD (L~ (Cage (C,n))) by A3, TARSKI:def 4;
hence contradiction by A4, GOBRD14:36; :: thesis: verum