let X be set ; :: thesis: ( Union <*X*> = X & meet <*X*> = X )
thus Union <*X*> = union (rng <*X*>) by CARD_3:def 4
.= union {X} by FINSEQ_1:55
.= X by ZFMISC_1:31 ; :: thesis: meet <*X*> = X
thus meet <*X*> = meet {X} by FINSEQ_1:55
.= X by SETFAM_1:11 ; :: thesis: verum