take the a_partition of X ; :: thesis: the a_partition of X is empty
thus the a_partition of X is empty ; :: thesis: verum