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) )
assume A1: x in BDD C ; :: thesis: x in RightComp (Cage C,n)
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 A1, XBOOLE_0:def 4;
then A2: 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 A3: not x in UBD (L~ (Cage C,n)) by A2, TARSKI:def 4;
A4: UBD (L~ (Cage C,n)) = union { E where E is Subset of (TOP-REAL 2) : E is_outside_component_of L~ (Cage C,n) } by JORDAN2C:def 6;
LeftComp (Cage C,n) is_outside_component_of L~ (Cage C,n) by GOBRD14:44;
then LeftComp (Cage C,n) in { E where E is Subset of (TOP-REAL 2) : E is_outside_component_of L~ (Cage C,n) } ;
then A5: not x in LeftComp (Cage C,n) by A3, A4, TARSKI:def 4;
A6: L~ (Cage C,n) = (Cl (LeftComp (Cage C,n))) \ (LeftComp (Cage C,n)) by GOBRD14:30;

now

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

end;

then not x in L~ (Cage C,n) by A6, XBOOLE_0:def 5;
hence x in RightComp (Cage C,n) by A1, A5, GOBRD14:28; :: thesis: verum