theorem :: TOPS_5:18

for X, Y being set holds
( ( X <> {} & Y = {} ) iff product (X --> Y) = {} )