theorem Th78: :: TOPGEN_5:78

for x being Real
for y being non negative Real
for r, a being positive Real st a <= 1 holds
(+ (x,y,r)) " [.0,a.[ = (Ball (|[x,y]|,(r * a))) /\ y>=0-plane