let X be non empty set ; :: thesis: 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 )
let G be Subset-Family of X; :: thesis: ( FinMeetCl G is with_non-empty_elements implies ( FinMeetCl G is filter_base of X & ex F being Filter of X st FinMeetCl G c= F ) )
assume A1: FinMeetCl G is with_non-empty_elements ; :: thesis: ( FinMeetCl G is filter_base of X & ex F being Filter of X st FinMeetCl G c= F )
reconsider FG = FinMeetCl G as Subset-Family of X ;
now :: thesis: for b1, b2 being Element of FG ex b being Element of FG st b c= b1 /\ b2
let b1, b2 be Element of FG; :: thesis: ex b being Element of FG st b c= b1 /\ b2
FinMeetCl FG c= FG by CANTOR_1:11;
then FG is cap-closed by Th02;
then reconsider b = b1 /\ b2 as Element of FG ;
( b is Element of FG & b c= b1 /\ b2 ) ;
hence ex b being Element of FG st b c= b1 /\ b2 ; :: thesis: verum
end;
then FG is quasi_basis ;
then reconsider FG = FG as filter_base of X by A1;
FG c= <.FG.) by def3;
hence ( FinMeetCl G is filter_base of X & ex F being Filter of X st FinMeetCl G c= F ) ; :: thesis: verum