theorem Th23: :: FUNCT_6:27

for X, Y being set st X <> {} holds
( Union (X --> Y) = Y & meet (X --> Y) = Y )