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

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