theorem Th13: :: SGRAPH1:13

for A being finite set holds TWOELEMENTSETS A is finite by Th9, FINSET_1:1;