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