let Y, SFX be set ; :: thesis: ( SFX is_finer_than {Y} implies for X being set st X in SFX holds
X c= Y )
assume A1: for X being set st X in SFX holds
ex Z being set st
( Z in {Y} & X c= Z ) ; :: according to SETFAM_1:def 2 :: thesis: for X being set st X in SFX holds
X c= Y
let X be set ; :: thesis: ( X in SFX implies X c= Y )
assume X in SFX ; :: thesis: X c= Y
then ex Z being set st
( Z in {Y} & X c= Z ) by A1;
hence X c= Y by TARSKI:def 1; :: thesis: verum