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

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

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

proof

union SFX c= union (SFX \ {{}})
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;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

proof

hence
union (SFX \ {{}}) = union SFX
by A1, XBOOLE_0:def 10; :: thesis: verum
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;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