let A be non empty set ; :: thesis: SmallestPartition A is_finer_than {A}
let X be set ; :: according to SETFAM_1:def 2 :: thesis: ( not X in SmallestPartition A or ex b₁ being set st
( b₁ in {A} & X c= b₁ ) )
assume A1: X in SmallestPartition A ; :: thesis: ex b₁ being set st
( b₁ in {A} & X c= b₁ )
take A ; :: thesis: ( A in {A} & X c= A )
thus ( A in {A} & X c= A ) by A1, TARSKI:def 1; :: thesis: verum