let x be set ; :: thesis: union {x} = x
A1: union {x} c= x

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in union {x} or y in x )
assume y in union {x} ; :: thesis: y in x
then ex Y being set st
( y in Y & Y in {x} ) by TARSKI:def 4;
hence y in x by TARSKI:def 1; :: thesis: verum

end;

x in {x} by TARSKI:def 1;
then x c= union {x} by Lm15;
hence union {x} = x by A1, XBOOLE_0:def 10; :: thesis: verum