let X be non empty set ; :: thesis: union (SmallestPartition X) = X
A0: SmallestPartition X = { {x} where x is Element of X : verum } by EQREL_1:37;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: X c= union (SmallestPartition X)

let o be object ; :: thesis: ( o in union (SmallestPartition X) implies o in X )
assume o in union (SmallestPartition X) ; :: thesis: o in X
then ex y being set st
( o in y & y in SmallestPartition X ) by TARSKI:def 4;
hence o in X ; :: thesis: verum

end;

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in X or o in union (SmallestPartition X) )
assume o in X ; :: thesis: o in union (SmallestPartition X)
then ( o in {o} & {o} in SmallestPartition X ) by A0, TARSKI:def 1;
hence o in union (SmallestPartition X) by TARSKI:def 4; :: thesis: verum