let n be Element of 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 set ; :: 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:44;
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 6;
assume A2: x in BDD C ; :: thesis: x in RightComp (Cage C,n)

A3: now

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

end;

BDD C misses UBD C by JORDAN2C:28;
then (BDD C) /\ (UBD C) = {} by XBOOLE_0:def 7;
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 Element of 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:30;
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:28; :: thesis: verum