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