:: deftheorem defines DOM URYSOHN1:def 3 :
DOM = ((halfline 0) \/ DYADIC) \/ (right_open_halfline 1);