let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis:
thus meet (BDD-Family C) c= C \/ (BDD C) :: according to XBOOLE_0:def 10 :: thesis:

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A1: x in meet (BDD-Family C) ; :: thesis:
COMPLEMENT (UBD-Family C) = BDD-Family C by Th20;
then ([#] the carrier of (TOP-REAL 2)) \ (union (UBD-Family C)) = meet (BDD-Family C) by SETFAM_1:33;
then not x in union (UBD-Family C) by A1, XBOOLE_0:def 5;
then A2: not x in UBD C by Th14;

suppose A3: not x in C ; :: thesis:

A4: (BDD C) \/ (UBD C) = C ` by JORDAN2C:27;
x in C ` by A1, A3, SUBSET_1:29;
then x in BDD C by A2, A4, XBOOLE_0:def 3;
hence x in C \/ (BDD C) by XBOOLE_0:def 3; :: thesis:

end;

suppose x in C ; :: thesis:

hence x in C \/ (BDD C) by XBOOLE_0:def 3; :: thesis:

end;

end;

end;

BDD C misses UBD C by JORDAN2C:24;
then A5: (BDD C) /\ (UBD C) = {} ;
A6: BDD C c= meet (BDD-Family C)

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A7: x in BDD C ; :: thesis:
then not x in UBD C by A5, XBOOLE_0:def 4;
then A8: not x in union (UBD-Family C) by Th14;
for Y being set st Y in BDD-Family C holds
x in Y

let Y be set ; :: thesis:
assume Y in BDD-Family C ; :: thesis:
then consider n being Nat such that
A9: Y = Cl (BDD (L~ (Cage (C,n)))) and
verum ;
LeftComp (Cage (C,n)) is_outside_component_of L~ (Cage (C,n)) by GOBRD14:34;
then A10: LeftComp (Cage (C,n)) in { B where B is Subset of (TOP-REAL 2) : B is_outside_component_of L~ (Cage (C,n)) } ;
BDD C misses L~ (Cage (C,n)) by Th19;
then (BDD C) /\ (L~ (Cage (C,n))) = {} ;
then A11: not x in L~ (Cage (C,n)) by A7, XBOOLE_0:def 4;
RightComp (Cage (C,n)) is_inside_component_of L~ (Cage (C,n)) by GOBRD14:35;
then A12: RightComp (Cage (C,n)) in { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of L~ (Cage (C,n)) } ;
UBD (L~ (Cage (C,n))) in UBD-Family C ;
then ( UBD (L~ (Cage (C,n))) = union { B where B is Subset of (TOP-REAL 2) : B is_outside_component_of L~ (Cage (C,n)) } & not x in UBD (L~ (Cage (C,n))) ) by A8, JORDAN2C:def 5, TARSKI:def 4;
then not x in LeftComp (Cage (C,n)) by A10, TARSKI:def 4;
then ( BDD (L~ (Cage (C,n))) = union { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of L~ (Cage (C,n)) } & x in RightComp (Cage (C,n)) ) by A7, A11, GOBRD14:18, JORDAN2C:def 4;
then A13: x in BDD (L~ (Cage (C,n))) by A12, TARSKI:def 4;
BDD (L~ (Cage (C,n))) c= Cl (BDD (L~ (Cage (C,n)))) by PRE_TOPC:18;
hence x in Y by A9, A13; :: thesis:

end;

hence x in meet (BDD-Family C) by SETFAM_1:def 1; :: thesis:

end;

C c= meet (BDD-Family C) by Th15;
hence C \/ (BDD C) c= meet (BDD-Family C) by A6, XBOOLE_1:8; :: thesis: