[#] K c= the carrier of X by SIMPLEX0:def 9;
then bool ([#] K) c= bool the carrier of X by ZFMISC_1:67;
hence A is Subset-Family of X by XBOOLE_1:1; :: thesis: verum