F . x c= the carrier of T ;
hence F . x is Subset of T ; :: thesis: verum