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 A2: y in union (SFX \ {{} }) ; :: thesis: y in union SFX
A3: ex z being set st
( y in z & z in SFX \ {{} } ) by A2, TARSKI:def 4;
thus y in union SFX by A3, TARSKI:def 4; :: thesis: verum

end;

A4: 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 A5: y in union SFX ; :: thesis: y in union (SFX \ {{} })
consider X being set such that
A6: y in X and
A7: X in SFX by A5, TARSKI:def 4;
A8: not X in {{} } by A6, TARSKI:def 1;
A9: X in SFX \ {{} } by A7, A8, XBOOLE_0:def 5;
thus y in union (SFX \ {{} }) by A6, A9, TARSKI:def 4; :: thesis: verum

end;

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