set F = meet (rng M);

A1: now :: thesis:

let Y be set ; :: thesis:
assume Y in rng M ; :: thesis:
then consider a being object such that
A2: a in dom M and
A3: M . a = Y by FUNCT_1:def 3;
M . a in Filt X by A2, FUNCT_1:102;
then consider FF being Filter of X such that
A4: M . a = FF ;
thus X in Y by A3, A4, CARD_FIL:5; :: thesis:

end;

let x be object ; :: thesis:
assume A5: x in meet (rng M) ; :: thesis:
set i0 = the Element of I;
( the Element of I in I & not I is empty ) ;
then A6: the Element of I in dom M by PARTFUN1:def 2;
then M . the Element of I in rng M by FUNCT_1:def 3;
then A7: x in M . the Element of I by A5, SETFAM_1:def 1;
M . the Element of I in Filt X by A6, FUNCT_1:102;
then consider F0 being Filter of X such that
A8: M . the Element of I = F0 ;
thus x in bool X by A7, A8; :: thesis:

end;

then meet (rng M) c= bool X ;
then reconsider F = meet (rng M) as non empty Subset-Family of X by A1, SETFAM_1:def 1;
A9: not {} in F

assume A10: {} in F ; :: thesis:
set i0 = the Element of I;
( the Element of I in I & not I is empty ) ;
then A11: the Element of I in dom M by PARTFUN1:def 2;
then A12: M . the Element of I in rng M by FUNCT_1:def 3;
M . the Element of I in Filt X by A11, FUNCT_1:102;
then consider F0 being Filter of X such that
A13: M . the Element of I = F0 ;
{} in F0 by A12, A10, SETFAM_1:def 1, A13;
hence contradiction by CARD_FIL:def 1; :: thesis:

end;

hereby :: thesis:

let Y1, Y2 be Subset of X; :: thesis:
assume that
A14: Y1 in F and
A15: Y2 in F ; :: thesis:

let Y be set ; :: thesis:
assume A16: Y in rng M ; :: thesis:
then Y in Filt X ;
then consider F0 being Filter of X such that
A17: Y = F0 ;
( Y1 in F0 & Y2 in F0 ) by A14, A15, A16, A17, SETFAM_1:def 1;
hence Y1 /\ Y2 in Y by A17, CARD_FIL:def 1; :: thesis:

end;

hence Y1 /\ Y2 in F by SETFAM_1:def 1; :: thesis:

end;

let Y1, Y2 be Subset of X; :: thesis:
assume that
A18: Y1 in F and
A19: Y1 c= Y2 ; :: thesis:

let Y be set ; :: thesis:
assume A20: Y in rng M ; :: thesis:
then Y in Filt X ;
then consider F0 being Filter of X such that
A21: Y = F0 ;
Y1 in Y by A18, A20, SETFAM_1:def 1;
hence Y2 in Y by A19, A21, CARD_FIL:def 1; :: thesis:

end;

hence Y2 in F by SETFAM_1:def 1; :: thesis:

end;

hence meet (rng M) is Filter of X by A9, CARD_FIL:def 1; :: thesis: