per cases ( Y = {} or Y <> {} ) ;
suppose Y = {} ; :: thesis: not PARTITIONS Y is empty
hence not PARTITIONS Y is empty by ; :: thesis: verum
end;
suppose Y <> {} ; :: thesis: not PARTITIONS Y is empty
then reconsider Y = Y as non empty set ;
A1: ( {Y} is Subset-Family of Y & union {Y} = Y ) by ;
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 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 ; :: 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 ; :: thesis: verum
end;
then {Y} is a_partition of Y by ;
hence not PARTITIONS Y is empty by Def3; :: thesis: verum
end;
end;