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 ) ) )

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

hence
{Y} is a_partition of Y
by A1, EQREL_1:def 4; :: thesis: verum
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 A2: A in {Y} ; :: thesis: ( A <> {} & ( for B being Subset of Y holds

( not B in {Y} or A = B or A misses B ) ) )

then A3: A = Y by TARSKI:def 1;

thus A <> {} by A2, 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 A3, TARSKI:def 1; :: thesis: verum

end;( not B in {Y} or A = B or A misses B ) ) ) )

assume A2: A in {Y} ; :: thesis: ( A <> {} & ( for B being Subset of Y holds

( not B in {Y} or A = B or A misses B ) ) )

then A3: A = Y by TARSKI:def 1;

thus A <> {} by A2, 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 A3, TARSKI:def 1; :: thesis: verum