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