let SFX be set ; :: thesis: union (SFX \ {{} }) = union SFX
A1: union (SFX \ {{} }) c= union SFX

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in union (SFX \ {{} }) or y in union SFX )
assume y in union (SFX \ {{} }) ; :: thesis: y in union SFX
then ex z being set st
( y in z & z in SFX \ {{} } ) by TARSKI:def 4;
hence y in union SFX by TARSKI:def 4; :: thesis: verum

end;

union SFX c= union (SFX \ {{} })

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in union SFX or y in union (SFX \ {{} }) )
assume y in union SFX ; :: thesis: y in union (SFX \ {{} })
then consider X being set such that
A6: y in X and
A7: X in SFX by TARSKI:def 4;
not X in {{} } by A6, TARSKI:def 1;
then X in SFX \ {{} } by A7, XBOOLE_0:def 5;
hence y in union (SFX \ {{} }) by A6, TARSKI:def 4; :: thesis: verum

end;

hence union (SFX \ {{} }) = union SFX by A1, XBOOLE_0:def 10; :: thesis: verum