:: deftheorem defines '<' BVFUNC_1:def 12 :
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds
( a '<' b iff for x being Element of Y st a . x = TRUE holds
b . x = TRUE );