let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); meet (BDD-Family C) = C \/ (BDD C)
thus
meet (BDD-Family C) c= C \/ (BDD C)
XBOOLE_0:def 10 C \/ (BDD C) c= meet (BDD-Family C)
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 ;
TARSKI:def 3 ( not x in BDD C or x in meet (BDD-Family C) )
assume A7:
x in BDD C
;
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 ;
( Y in BDD-Family C implies x in Y )
assume
Y in BDD-Family C
;
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;
verum
end;
hence
x in meet (BDD-Family C)
by SETFAM_1:def 1;
verum
end;
C c= meet (BDD-Family C)
by Th15;
hence
C \/ (BDD C) c= meet (BDD-Family C)
by A6, XBOOLE_1:8; verum