let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: meet (BDD-Family C) = C \/ (BDD C)
BDD C misses UBD C by JORDAN2C:28;
then A1: (BDD C) /\ (UBD C) = {} by XBOOLE_0:def 7;
thus meet (BDD-Family C) c= C \/ (BDD C) :: according to XBOOLE_0:def 10 :: thesis: C \/ (BDD C) c= meet (BDD-Family C)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in meet (BDD-Family C) or x in C \/ (BDD C) )
assume A2: x in meet (BDD-Family C) ; :: thesis: x in C \/ (BDD C)
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:47;
then not x in union (UBD-Family C) by A2, XBOOLE_0:def 5;
then A3: not x in UBD C by Th14;

per cases ( not x in C or x in C ) ;

suppose not x in C ; :: thesis: x in C \/ (BDD C)

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

end;

suppose x in C ; :: thesis: x in C \/ (BDD C)

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

end;

end;

end;

A5: BDD C c= meet (BDD-Family C)

proof

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

proof

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

end;

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

end;

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