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