let A be set ; :: thesis: for X being Subset of A holds X = union { {x} where x is Element of A : x in X }
let X be Subset of A; :: thesis: X = union { {x} where x is Element of A : x in X }
thus X c= union { {x} where x is Element of A : x in X } :: according to XBOOLE_0:def 10 :: thesis: union { {x} where x is Element of A : x in X } c= X

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in X or a in union { {x} where x is Element of A : x in X } )
assume A1: a in X ; :: thesis: a in union { {x} where x is Element of A : x in X }
set Y = {a};
A2: a in {a} by TARSKI:def 1;
{a} in { {x} where x is Element of A : x in X } by A1;
hence a in union { {x} where x is Element of A : x in X } by A2, TARSKI:def 4; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union { {x} where x is Element of A : x in X } or a in X )
assume a in union { {x} where x is Element of A : x in X } ; :: thesis: a in X
then consider Y being set such that
A3: a in Y and
A4: Y in { {x} where x is Element of A : x in X } by TARSKI:def 4;
ex x being Element of A st
( Y = {x} & x in X ) by A4;
hence a in X by A3, TARSKI:def 1; :: thesis: verum