:: deftheorem defines -pr1 FOMODEL0:def 5 :
for D being set holds D -pr1 = pr1 (D,D);