theorem :: INTEGRA2:7

for X being real-membered set
for a being Real holds
( X is empty iff a ** X is empty ) ;