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 Nat such that
A1: P = Cl (BDD (L~ (Cage (C,k)))) ;
P = Cl (RightComp (Cage (C,k))) by A1, GOBRD14:37;
then A2: P = (RightComp (Cage (C,k))) \/ (L~ (Cage (C,k))) by GOBRD14:21;
(P `) /\ ((LeftComp (Cage (C,k))) `) = (P \/ (LeftComp (Cage (C,k)))) ` by XBOOLE_1:53
.= ([#] the carrier of (TOP-REAL 2)) ` by A2, GOBRD14:15
.= {} the carrier of (TOP-REAL 2) by XBOOLE_1:37 ;
then A3: P ` misses (LeftComp (Cage (C,k))) ` ;
( L~ (Cage (C,k)) misses LeftComp (Cage (C,k)) & RightComp (Cage (C,k)) misses LeftComp (Cage (C,k)) ) by GOBRD14:14, SPRECT_3:26;
then P misses LeftComp (Cage (C,k)) by A2, XBOOLE_1:70;
then P ` = LeftComp (Cage (C,k)) by A3, SUBSET_1:25;
then P ` = UBD (L~ (Cage (C,k))) by GOBRD14:36;
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 Nat such that
A4: P ` = UBD (L~ (Cage (C,k))) ;
A5: P ` = LeftComp (Cage (C,k)) by A4, GOBRD14:36;
then ( P ` misses RightComp (Cage (C,k)) & P ` misses L~ (Cage (C,k)) ) by GOBRD14:14, SPRECT_3:26;
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:21;
((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:21
.= ([#] the carrier of (TOP-REAL 2)) ` by A5, GOBRD14:15
.= {} the carrier of (TOP-REAL 2) by XBOOLE_1:37 ;
then (P `) ` misses (Cl (RightComp (Cage (C,k)))) ` ;
then (P `) ` = Cl (RightComp (Cage (C,k))) by A6, SUBSET_1:25;
then P = Cl (BDD (L~ (Cage (C,k)))) by GOBRD14:37;
hence P in BDD-Family C ; :: thesis: verum
end;
hence COMPLEMENT (UBD-Family C) = BDD-Family C by SETFAM_1:def 7; :: thesis: verum