theorem Th9: :: SGRAPH1:9

for A being set holds TWOELEMENTSETS A c= bool A