theorem :: BVFUNC_1:66

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