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