per cases ( Y = {} or Y <> {} ) ;

suppose A1: Y = {} ; :: thesis: not PARTITIONS Y is empty

thus not PARTITIONS Y is empty by A1, Def3, EQREL_1:54; :: thesis: verum

end;

suppose A2: Y <> {} ; :: thesis: not PARTITIONS Y is empty

reconsider Y = Y as non empty set by A2;
A3: ( {Y} is Subset-Family of Y & union {Y} = Y ) by ZFMISC_1:31, ZFMISC_1:80;
A4: for A being Subset of Y st A in {Y} holds
( A <> {} & ( for B being Subset of Y holds
( not B in {Y} or A = B or A misses B ) ) )

proof

let A be Subset of Y; :: thesis: ( A in {Y} implies ( A <> {} & ( for B being Subset of Y holds
( not B in {Y} or A = B or A misses B ) ) ) )
assume A5: A in {Y} ; :: thesis: ( A <> {} & ( for B being Subset of Y holds
( not B in {Y} or A = B or A misses B ) ) )
A6: A = Y by A5, TARSKI:def 1;
thus A <> {} by A5, TARSKI:def 1; :: thesis: for B being Subset of Y holds
( not B in {Y} or A = B or A misses B )
let B be Subset of Y; :: thesis: ( not B in {Y} or A = B or A misses B )
assume A7: B in {Y} ; :: thesis: ( A = B or A misses B )
thus ( A = B or A misses B ) by A6, A7, TARSKI:def 1; :: thesis: verum

end;

A8: {Y} is a_partition of Y by A3, A4, EQREL_1:def 6;
thus not PARTITIONS Y is empty by A8, Def3; :: thesis: verum

end;

end;