:: deftheorem defines typed| FOMODEL0:def 27 :
for A being set
for R being Relation holds R typed| A = R | A;