let P be a_partition of X; :: thesis: not P is empty
consider x being Element of X;
union P = X by Def6;
then ex A being set st
( x in A & A in P ) by TARSKI:def 4;
hence not P is empty ; :: thesis: verum