consider p being a_partition of X;
reconsider P = {p} as Part-Family of X by Th49;
take P ; :: thesis: not P is empty
thus not P is empty ; :: thesis: verum