reconsider X = x as set by TARSKI:1;
A1: union {X} c= X

proof

let y be object ; :: 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 Lm14;
hence union {x} = x by A1, XBOOLE_0:def 10; :: thesis: verum