:: deftheorem defines typed\ FOMODEL0:def 16 :
for A, B being set holds A typed\ B = A \ B;