let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: C c= meet (BDD-Family C)
for Z being set st Z in BDD-Family C holds
C c= Z
proof
let Z be set ; :: thesis: ( Z in BDD-Family C implies C c= Z )
assume Z in BDD-Family C ; :: thesis: C c= Z
then consider k being Nat such that
A1: Z = Cl (BDD (L~ (Cage (C,k)))) ;
( C c= BDD (L~ (Cage (C,k))) & BDD (L~ (Cage (C,k))) c= Cl (BDD (L~ (Cage (C,k)))) ) by Th12, PRE_TOPC:18;
hence C c= Z by A1; :: thesis: verum
end;
hence C c= meet (BDD-Family C) by SETFAM_1:5; :: thesis: verum