theorem :: CARDFIL3:1

for I being set holds {} is Element of Fin I