theorem Th89: :: ZFMISC_1:90

for X, Y being set holds
( [:X,Y:] = {} iff ( X = {} or Y = {} ) )