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