theorem :: ZFMISC_1:36

for x1, x2 being object
for Z being set holds
( Z c= {x1,x2} iff ( Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2} ) ) by Lm13;