:: deftheorem defines fixpoints1 FOMODEL0:def 36 :
for R being set holds fixpoints1 R = proj1 (R /\ (id ((proj1 R) /\ (proj2 R))));