theorem :: GATE_1:33

for a, b, c, d, e, f, g being set holds
( ( not a is empty or not b is empty or not c is empty or not d is empty or not e is empty or not f is empty or not g is empty ) iff not OR7 (a,b,c,d,e,f,g) is empty ) by Def27;