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