reconsider A = {} as Subset-Family of by XBOOLE_1:2;
( union A = {} & ( for a being Subset of st a in A holds
( a <> {} & ( for b being Subset of holds
( not b in A or a = b or a misses b ) ) ) ) ) ;
hence {} is a_partition of {} by Def6; :: thesis: verum