A1: {Y} is Subset-Family of Y by ZFMISC_1:80;
A2: union {Y} = Y by ZFMISC_1:31;
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 A3: A in {Y} ; :: thesis: ( A <> {} & ( for B being Subset of Y holds
( not B in {Y} or A = B or A misses B ) ) )
then A4: A = Y by TARSKI:def 1;
thus A <> {} by A3, 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 B in {Y} ; :: thesis: ( A = B or A misses B )
hence ( A = B or A misses B ) by A4, TARSKI:def 1; :: thesis: verum

end;

hence {Y} is a_partition of Y by A1, A2, EQREL_1:def 6; :: thesis: verum