let x be set ; :: thesis: union {{},{x}} = {x}
{x} = union (bool {x}) by ZFMISC_1:81;
hence union {{},{x}} = {x} by ZFMISC_1:24; :: thesis: verum