let SFX be set ; :: thesis: ( SFX is_finer_than {} implies SFX = {} )

assume A1: for X being set st X in SFX holds

ex Y being set st

( Y in {} & X c= Y ) ; :: according to SETFAM_1:def 2 :: thesis: SFX = {}

set x = the Element of SFX;

assume not SFX = {} ; :: thesis: contradiction

then ex Y being set st

( Y in {} & the Element of SFX c= Y ) by A1;

hence contradiction ; :: thesis: verum

assume A1: for X being set st X in SFX holds

ex Y being set st

( Y in {} & X c= Y ) ; :: according to SETFAM_1:def 2 :: thesis: SFX = {}

set x = the Element of SFX;

assume not SFX = {} ; :: thesis: contradiction

then ex Y being set st

( Y in {} & the Element of SFX c= Y ) by A1;

hence contradiction ; :: thesis: verum