theorem Th1: :: MATRIX_9:1

for a, A being set st a in A holds
{a} in Fin A