A1: ( {Y} is Subset-Family of Y & union {Y} = Y ) by ZFMISC_1:25, ZFMISC_1:68;
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 ) ) )

let A be Subset of Y; :: thesis:
assume A2: A in {Y} ; :: thesis:
then A3: A = Y by TARSKI:def 1;
thus A <> {} by A2, TARSKI:def 1; :: thesis:
let B be Subset of Y; :: thesis:
assume B in {Y} ; :: thesis:
hence ( A = B or A misses B ) by A3, TARSKI:def 1; :: thesis:

end;

hence {Y} is a_partition of Y by A1, EQREL_1:def 4; :: thesis: