let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: COMPLEMENT (UBD-Family C) = BDD-Family C
for P being Subset of (TOP-REAL 2) holds
( P in BDD-Family C iff P ` in UBD-Family C )

proof

let P be Subset of (TOP-REAL 2); :: thesis: ( P in BDD-Family C iff P ` in UBD-Family C )
thus ( P in BDD-Family C implies P ` in UBD-Family C ) :: thesis: ( P ` in UBD-Family C implies P in BDD-Family C )

proof

assume P in BDD-Family C ; :: thesis: P ` in UBD-Family C
then consider k being Element of NAT such that
A1: P = Cl (BDD (L~ (Cage (C,k)))) ;
P = Cl (RightComp (Cage (C,k))) by A1, GOBRD14:47;
then A2: P = (RightComp (Cage (C,k))) \/ (L~ (Cage (C,k))) by GOBRD14:31;
(P `) /\ ((LeftComp (Cage (C,k))) `) = (P \/ (LeftComp (Cage (C,k)))) ` by XBOOLE_1:53
.= ([#] the carrier of (TOP-REAL 2)) ` by A2, GOBRD14:25
.= {} the carrier of (TOP-REAL 2) by XBOOLE_1:37 ;
then A3: P ` misses (LeftComp (Cage (C,k))) ` by XBOOLE_0:def 7;
( L~ (Cage (C,k)) misses LeftComp (Cage (C,k)) & RightComp (Cage (C,k)) misses LeftComp (Cage (C,k)) ) by GOBRD14:24, SPRECT_3:43;
then P misses LeftComp (Cage (C,k)) by A2, XBOOLE_1:70;
then P ` = LeftComp (Cage (C,k)) by A3, SUBSET_1:46;
then P ` = UBD (L~ (Cage (C,k))) by GOBRD14:46;
hence P ` in UBD-Family C ; :: thesis: verum

end;

assume P ` in UBD-Family C ; :: thesis: P in BDD-Family C
then consider k being Element of NAT such that
A4: P ` = UBD (L~ (Cage (C,k))) ;
A5: P ` = LeftComp (Cage (C,k)) by A4, GOBRD14:46;
then ( P ` misses RightComp (Cage (C,k)) & P ` misses L~ (Cage (C,k)) ) by GOBRD14:24, SPRECT_3:43;
then P ` misses (RightComp (Cage (C,k))) \/ (L~ (Cage (C,k))) by XBOOLE_1:70;
then A6: P ` misses Cl (RightComp (Cage (C,k))) by GOBRD14:31;
((P `) `) /\ ((Cl (RightComp (Cage (C,k)))) `) = ((P `) \/ (Cl (RightComp (Cage (C,k))))) ` by XBOOLE_1:53
.= ((P `) \/ ((RightComp (Cage (C,k))) \/ (L~ (Cage (C,k))))) ` by GOBRD14:31
.= ([#] the carrier of (TOP-REAL 2)) ` by A5, GOBRD14:25
.= {} the carrier of (TOP-REAL 2) by XBOOLE_1:37 ;
then (P `) ` misses (Cl (RightComp (Cage (C,k)))) ` by XBOOLE_0:def 7;
then (P `) ` = Cl (RightComp (Cage (C,k))) by A6, SUBSET_1:46;
then P = Cl (BDD (L~ (Cage (C,k)))) by GOBRD14:47;
hence P in BDD-Family C ; :: thesis: verum

end;

hence COMPLEMENT (UBD-Family C) = BDD-Family C by SETFAM_1:def 8; :: thesis: verum