set F = meet (rng M);

A1: now :: thesis: for Y being set st Y in rng M holds
X in Y

let Y be set ; :: thesis: ( Y in rng M implies X in Y )
assume Y in rng M ; :: thesis: X in Y
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: verum

end;

now :: thesis: for x being object st x in meet (rng M) holds
x in bool X

let x be object ; :: thesis: ( x in meet (rng M) implies x in bool X )
assume A5: x in meet (rng M) ; :: thesis: x in bool X
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: verum

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

proof

assume A10: {} in F ; :: thesis: contradiction
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: verum

end;

now :: thesis: ( ( for Y1, Y2 being Subset of X st Y1 in F & Y2 in F holds
Y1 /\ Y2 in F ) & ( for Y1, Y2 being Subset of X st Y1 in F & Y1 c= Y2 holds
Y2 in F ) )

hereby :: thesis: for Y1, Y2 being Subset of X st Y1 in F & Y1 c= Y2 holds
Y2 in F

let Y1, Y2 be Subset of X; :: thesis: ( Y1 in F & Y2 in F implies Y1 /\ Y2 in F )
assume that
A14: Y1 in F and
A15: Y2 in F ; :: thesis: Y1 /\ Y2 in F

now :: thesis: for Y being set st Y in rng M holds
Y1 /\ Y2 in Y

let Y be set ; :: thesis: ( Y in rng M implies Y1 /\ Y2 in Y )
assume A16: Y in rng M ; :: thesis: Y1 /\ Y2 in Y
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: verum

end;

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

end;

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

now :: thesis: for Y being set st Y in rng M holds
Y2 in Y

let Y be set ; :: thesis: ( Y in rng M implies Y2 in Y )
assume A20: Y in rng M ; :: thesis: Y2 in Y
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: verum

end;

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

end;

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