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