let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: meet (BDD-Family C) = C \/ (BDD C)
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 A1: 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 A1, XBOOLE_0:def 5;
then A2: not x in UBD C by Th14;

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

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

A4: (BDD C) \/ (UBD C) = C ` by JORDAN2C:31;
x in C ` by A1, A3, SUBSET_1:50;
then x in BDD C by A2, 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;

BDD C misses UBD C by JORDAN2C:28;
then A5: (BDD C) /\ (UBD C) = {} by XBOOLE_0:def 7;
A6: 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 A7: x in BDD C ; :: thesis: x in meet (BDD-Family C)
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

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
A9: Y = Cl (BDD (L~ (Cage C,n))) and
verum ;
LeftComp (Cage C,n) is_outside_component_of L~ (Cage C,n) by GOBRD14:44;
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)) = {} by XBOOLE_0:def 7;
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:45;
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 6, 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:28, JORDAN2C:def 5;
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:48;
hence x in Y by A9, A13; :: 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 A6, XBOOLE_1:8; :: thesis: verum