theorem :: FUNCT_5:16

for X being set holds
( proj1 X = {} iff proj2 X = {} )