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

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