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 object ; :: 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:33;
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: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: 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:24;
then A5: (BDD C) /\ (UBD C) = {} ;
A6: BDD C c= meet (BDD-Family C)

proof

let x be object ; :: 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 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: 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