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