:: deftheorem defines |1 FOMODEL0:def 28 :
for X, P being set holds P |1 X = P /\ [:X,(proj2 P):];