consider p being a_partition of X;
take p ; :: thesis: ( not p is empty & p is finite )
thus ( not p is empty & p is finite ) ; :: thesis: verum