Union Un c= bool the carrier of T ;
hence Union Un is Subset-Family of T ; :: thesis: verum