let SFX be set ; :: thesis: SFX is_finer_than UNION (SFX,SFX)

let X be set ; :: according to SETFAM_1:def 2 :: thesis: ( X in SFX implies ex Y being set st

( Y in UNION (SFX,SFX) & X c= Y ) )

assume A1: X in SFX ; :: thesis: ex Y being set st

( Y in UNION (SFX,SFX) & X c= Y )

take X ; :: thesis: ( X in UNION (SFX,SFX) & X c= X )

X = X \/ X ;

hence ( X in UNION (SFX,SFX) & X c= X ) by A1, Def4; :: thesis: verum

let X be set ; :: according to SETFAM_1:def 2 :: thesis: ( X in SFX implies ex Y being set st

( Y in UNION (SFX,SFX) & X c= Y ) )

assume A1: X in SFX ; :: thesis: ex Y being set st

( Y in UNION (SFX,SFX) & X c= Y )

take X ; :: thesis: ( X in UNION (SFX,SFX) & X c= X )

X = X \/ X ;

hence ( X in UNION (SFX,SFX) & X c= X ) by A1, Def4; :: thesis: verum