[#] 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

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