{x,y,z} is Subset of X by SUBSET_1:57;
hence {.y,z,.} is Element of Fin X by FINSUB_1:def 5; :: thesis: verum