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 } ;
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 ; :: 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;
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 )
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