:: deftheorem defines <= BVFUNC_1:def 1 :
for k, l being boolean object holds
( k <= l iff k => l = TRUE );