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

proof

let y be object ; :: 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 object ; :: 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
A2: y in X and
A3: X in SFX by TARSKI:def 4;
not X in {{}} by A2, TARSKI:def 1;
then X in SFX \ {{}} by A3, XBOOLE_0:def 5;
hence y in union (SFX \ {{}}) by A2, TARSKI:def 4; :: thesis: verum

end;

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