:: deftheorem defines BDD JORDAN2C:def 4 :
for n being Nat
for A being Subset of (TOP-REAL n) holds BDD A = union { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A } ;