let X be set ; :: thesis: ( Union <*X*> = X & meet <*X*> = X )
thus Union <*X*> = union (rng <*X*>)
.= union {X} by FINSEQ_1:38
.= X by ZFMISC_1:25 ; :: thesis: meet <*X*> = X
thus meet <*X*> = meet {X} by FINSEQ_1:38
.= X by SETFAM_1:10 ; :: thesis: verum