{x} is Subset of X by SUBSET_1:63;
hence {x} is Element of Fin X by FINSUB_1:def 5; :: thesis: verum