theorem Th6: :: ZFMISC_1:6

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