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

hence {X} is a_partition of X by A1, Def4; :: thesis: verum

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

union A1 = X
;
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;( 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

hence {X} is a_partition of X by A1, Def4; :: thesis: verum