theorem :: ZFMISC_1:22

for x1, x2, y1, y2 being object holds
( not {x1,x2} c= {y1,y2} or x1 = y1 or x1 = y2 )