let Y be set ; :: thesis: ( Union ({} --> Y) = {} & meet ({} --> Y) = {} )
union (rng ({} --> Y)) = {} by ZFMISC_1:2;
hence ( Union ({} --> Y) = {} & meet ({} --> Y) = {} ) by CARD_3:def 4, SETFAM_1:def 1; :: thesis: verum