let X be non empty set ; :: thesis: 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 )
let G be Subset-Family of X; :: thesis: for F being Filter of X st G c= F holds
( FinMeetCl G c= F & FinMeetCl G is with_non-empty_elements )
let F be Filter of X; :: thesis: ( G c= F implies ( FinMeetCl G c= F & FinMeetCl G is with_non-empty_elements ) )
assume A1: G c= F ; :: thesis: ( FinMeetCl G c= F & FinMeetCl G is with_non-empty_elements )
A2: FinMeetCl G c= FinMeetCl F by A1, CANTOR_1:14;
FinMeetCl F c= F by Th02, CARD_FIL:5;
hence FinMeetCl G c= F by A2; :: thesis: FinMeetCl G is with_non-empty_elements
hence FinMeetCl G is with_non-empty_elements by CARD_FIL:def 1; :: thesis: verum