theorem :: ZFMISC_1:107

for x being object
for X being set st X <> {} holds
( [:{x},X:] <> {} & [:X,{x}:] <> {} ) by Th89;