let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD C c= RightComp (Cage (C,n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: BDD C c= RightComp (Cage (C,n))
set f = Cage (C,n);
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in BDD C or x in RightComp (Cage (C,n)) )
LeftComp (Cage (C,n)) is_outside_component_of L~ (Cage (C,n)) by GOBRD14:34;
then A1: ( UBD (L~ (Cage (C,n))) = union { E where E is Subset of (TOP-REAL 2) : E is_outside_component_of L~ (Cage (C,n)) } & LeftComp (Cage (C,n)) in { E where E is Subset of (TOP-REAL 2) : E is_outside_component_of L~ (Cage (C,n)) } ) by JORDAN2C:def 5;
assume A2: x in BDD C ; :: thesis: x in RightComp (Cage (C,n))

A3: now :: thesis: not x in Cl (LeftComp (Cage (C,n)))

assume x in Cl (LeftComp (Cage (C,n))) ; :: thesis: contradiction
then BDD C meets LeftComp (Cage (C,n)) by A2, PRE_TOPC:def 7;
hence contradiction by Th16; :: thesis: verum

end;

BDD C misses UBD C by JORDAN2C:24;
then (BDD C) /\ (UBD C) = {} ;
then not x in UBD C by A2, XBOOLE_0:def 4;
then A4: not x in union (UBD-Family C) by Th14;
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 A4, TARSKI:def 4;
then A5: not x in LeftComp (Cage (C,n)) by A1, TARSKI:def 4;
L~ (Cage (C,n)) = (Cl (LeftComp (Cage (C,n)))) \ (LeftComp (Cage (C,n))) by GOBRD14:20;
then not x in L~ (Cage (C,n)) by A3, XBOOLE_0:def 5;
hence x in RightComp (Cage (C,n)) by A2, A5, GOBRD14:18; :: thesis: verum