let X be non empty set ; :: thesis: SmallestPartition X = { {x} where x is Element of X : verum }

set Y = { {x} where x is Element of X : verum } ;

assume x in { {x} where x is Element of X : verum } ; :: thesis: x in SmallestPartition X

then consider y being Element of X such that

A3: x = {y} ;

Class ((id X),y) = x by A3, Th25;

hence x in SmallestPartition X by Def3; :: thesis: verum

set Y = { {x} where x is Element of X : verum } ;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { {x} where x is Element of X : verum } c= SmallestPartition X

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { {x} where x is Element of X : verum } or x in SmallestPartition X )let x be object ; :: thesis: ( x in SmallestPartition X implies x in { {x} where x is Element of X : verum } )

assume x in SmallestPartition X ; :: thesis: x in { {x} where x is Element of X : verum }

then consider y being object such that

A1: y in X and

A2: x = Class ((id X),y) by Def3;

x = {y} by A1, A2, Th25;

hence x in { {x} where x is Element of X : verum } by A1; :: thesis: verum

end;assume x in SmallestPartition X ; :: thesis: x in { {x} where x is Element of X : verum }

then consider y being object such that

A1: y in X and

A2: x = Class ((id X),y) by Def3;

x = {y} by A1, A2, Th25;

hence x in { {x} where x is Element of X : verum } by A1; :: thesis: verum

assume x in { {x} where x is Element of X : verum } ; :: thesis: x in SmallestPartition X

then consider y being Element of X such that

A3: x = {y} ;

Class ((id X),y) = x by A3, Th25;

hence x in SmallestPartition X by Def3; :: thesis: verum