take {X} ; :: thesis: X c= union {X}
thus X c= union {X} by ZFMISC_1:25; :: thesis: verum