let a, A be set ; :: thesis: ( a in A implies {a} in Fin A )
assume a in A ; :: thesis: {a} in Fin A
then {a} c= A by ZFMISC_1:31;
hence {a} in Fin A by FINSUB_1:def 5; :: thesis: verum