theorem :: BVFUNC_1:67

for x, y being boolean object st 'not' x = TRUE holds
x => y = TRUE ;