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 Def4; :: thesis: verum