theorem :: SRINGS_5:103

for r being Real
for x being Element of REAL 0 holds
( Intervals (x,r) is empty & product (Intervals (x,r)) = {{}} ) by CARD_3:10;