[#] K c= the carrier of X by SIMPLEX0:def 9;
hence A is Subset of X by XBOOLE_1:1; :: thesis: verum