consider x being Element of X;
reconsider P = Class (nabla X) as a_partition of X ;
take P ; :: thesis: not P is empty
thus not P is empty ; :: thesis: verum