theorem :: GATE_1:5
for a, b being set holds
( ( not a is empty or not b is empty ) iff not OR2 (a,b) is empty ) ;