:: deftheorem Def37 defines constanT FOMODEL0:def 37 :
for X being set holds
( X is constanT iff proj2 X is trivial );