theorem Th17: :: YELLOW_9:17

for X being set
for A being empty Subset-Family of X holds FinMeetCl A = {X}