theorem :: BVFUNC_1:65

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