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