:: deftheorem defines Coim RELAT_1:def 17 :
for R being Relation
for x being object holds Coim (R,x) = R " {x};