:: deftheorem defines .:1 FOMODEL0:def 33 :
for X, Y being set holds X .:1 Y = proj2 (X |1 Y);