set p = the a_partition of X;

reconsider P = { the a_partition of X} as Part-Family of X by Th40;

take P ; :: thesis: not P is empty

thus not P is empty ; :: thesis: verum

reconsider P = { the a_partition of X} as Part-Family of X by Th40;

take P ; :: thesis: not P is empty

thus not P is empty ; :: thesis: verum