theorem Th13: :: FINSUB_1:13

for A being set holds Fin A c= bool A