let SFX be set ; :: thesis: DIFFERENCE (SFX,SFX) is_finer_than SFX

let X be set ; :: according to SETFAM_1:def 2 :: thesis: ( X in DIFFERENCE (SFX,SFX) implies ex Y being set st

( Y in SFX & X c= Y ) )

assume X in DIFFERENCE (SFX,SFX) ; :: thesis: ex Y being set st

( Y in SFX & X c= Y )

then consider Z1, Z2 being set such that

A1: Z1 in SFX and

Z2 in SFX and

A2: X = Z1 \ Z2 by Def6;

take Z1 ; :: thesis: ( Z1 in SFX & X c= Z1 )

thus ( Z1 in SFX & X c= Z1 ) by A1, A2; :: thesis: verum

let X be set ; :: according to SETFAM_1:def 2 :: thesis: ( X in DIFFERENCE (SFX,SFX) implies ex Y being set st

( Y in SFX & X c= Y ) )

assume X in DIFFERENCE (SFX,SFX) ; :: thesis: ex Y being set st

( Y in SFX & X c= Y )

then consider Z1, Z2 being set such that

A1: Z1 in SFX and

Z2 in SFX and

A2: X = Z1 \ Z2 by Def6;

take Z1 ; :: thesis: ( Z1 in SFX & X c= Z1 )

thus ( Z1 in SFX & X c= Z1 ) by A1, A2; :: thesis: verum