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