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