take X ; :: according to SETFAM_1:def 10 :: thesis: X in bool X
thus X in bool X by ZFMISC_1:def 1; :: thesis: verum