set p = the a_partition of X;
take the a_partition of X ; :: thesis: ( not the a_partition of X is empty & the a_partition of X is finite )
thus ( not the a_partition of X is empty & the a_partition of X is finite ) ; :: thesis: verum