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

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