let X be non empty set ; :: thesis: {X} is a_partition of X
reconsider A1 = {X} as Subset-Family of X by ZFMISC_1:68;
A1: for A being Subset of X st A in A1 holds
( A <> {} & ( for B being Subset of X holds
( not B in A1 or A = B or A misses B ) ) )
proof
let A be Subset of X; :: thesis: ( A in A1 implies ( A <> {} & ( for B being Subset of X holds
( not B in A1 or A = B or A misses B ) ) ) )
assume A2: A in A1 ; :: thesis: ( A <> {} & ( for B being Subset of X holds
( not B in A1 or A = B or A misses B ) ) )
hence A <> {} by TARSKI:def 1; :: thesis: for B being Subset of X holds
( not B in A1 or A = B or A misses B )
let B be Subset of X; :: thesis: ( not B in A1 or A = B or A misses B )
assume B in A1 ; :: thesis: ( A = B or A misses B )
then B = X by TARSKI:def 1;
hence ( A = B or A misses B ) by A2, TARSKI:def 1; :: thesis: verum
end;
union A1 = X ;
hence {X} is a_partition of X by A1, Def4; :: thesis: verum