theorem Th07: :: COUSIN2:7

for a, e being Real
for b, c, d being non negative Real st a <= (b * c) * d & d < e / ((2 * b) * |.c.|) holds
a <= e / 2