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_{1} being set st

( b_{1} in {A} & X c= b_{1} ) )

assume A1: X in SmallestPartition A ; :: thesis: ex b_{1} being set st

( b_{1} in {A} & X c= b_{1} )

take A ; :: thesis: ( A in {A} & X c= A )

thus ( A in {A} & X c= A ) by A1, TARSKI:def 1; :: thesis: verum

let X be set ; :: according to SETFAM_1:def 2 :: thesis: ( not X in SmallestPartition A or ex b

( b

assume A1: X in SmallestPartition A ; :: thesis: ex b

( b

take A ; :: thesis: ( A in {A} & X c= A )

thus ( A in {A} & X c= A ) by A1, TARSKI:def 1; :: thesis: verum