let A be non empty 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 set ; :: 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 set ; :: 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 & Y in { {x} where x is Element of A : x in X } ) by TARSKI:def 4;
consider x being Element of A such that
A4: ( Y = {x} & x in X ) by A3;
thus a in X by A3, A4, TARSKI:def 1; :: thesis: verum