theorem :: CARDFIL2:10

for X being set
for S being Subset-Family of X st FinMeetCl S is with_non-empty_elements holds
S is with_non-empty_elements