theorem Th21: :: YELLOW_9:21

for X being set
for A being Subset-Family of X holds UniCl (FinMeetCl (UniCl A)) = UniCl (FinMeetCl A)