let P be a_partition of {} ; :: thesis: P = {}
assume not P = {} ; :: thesis: contradiction
then consider Z being object such that
A1: Z in P by XBOOLE_0:def 1;
Z <> {} by A1, Def4;
hence contradiction by A1; :: thesis: verum