reconsider n' = n as Element of NAT by ORDINAL1:def 13;
(Finf A) . n' c= the carrier of T ;
hence (Finf A) . n is Subset of T ; :: thesis: verum