theorem :: CARDFIL2:11

for X being non empty set
for G being Subset-Family of X
for F being Filter of X st G c= F holds
( FinMeetCl G c= F & FinMeetCl G is with_non-empty_elements )