:: deftheorem defines fixpoints FOMODEL0:def 35 :
for R being set holds fixpoints R = proj1 (R /\ (id (proj1 R)));