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