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

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