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