let SFX be set ; :: thesis: {} is_finer_than SFX
let X be set ; :: according to SETFAM_1:def 2 :: thesis: ( X in {} implies ex Y being set st
( Y in SFX & X c= Y ) )
assume X in {} ; :: thesis: ex Y being set st
( Y in SFX & X c= Y )
hence ex Y being set st
( Y in SFX & X c= Y ) ; :: thesis: verum