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