:: deftheorem Def1 defines with_cardinal_domain COUNTERS:def 13 :
for R being Relation holds
( R is with_cardinal_domain iff ex c being Cardinal st dom R = c );