set D = { q where q is Element of : p [= q } ;
p in { q where q is Element of : p [= q } ;
then reconsider F = { q where q is Element of : p [= q } as non empty set ;
F c= the carrier of L

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in F or x in the carrier of L )
assume x in F ; :: thesis: x in the carrier of L
then ex q being Element of st
( x = q & p [= q ) ;
hence x in the carrier of L ; :: thesis: verum

end;

then reconsider F = F as non empty Subset of ;

A1: now

let r, q be Element of ; :: thesis: ( r in F & q in F implies r "/\" q in F )
assume r in F ; :: thesis: ( q in F implies r "/\" q in F )
then ex r1 being Element of st
( r = r1 & p [= r1 ) ;
then A2: p "/\" p [= r "/\" p by LATTICES:27;
assume q in F ; :: thesis: r "/\" q in F
then ex q1 being Element of st
( q = q1 & p [= q1 ) ;
then A3: p "/\" r [= q "/\" r by LATTICES:27;
p "/\" p = p by LATTICES:18;
then p [= r "/\" q by A3, A2, LATTICES:25;
hence r "/\" q in F ; :: thesis: verum

end;

now

let r, q be Element of ; :: thesis: ( r in F & r [= q implies q in F )
assume r in F ; :: thesis: ( r [= q implies q in F )
then A4: ex r1 being Element of st
( r = r1 & p [= r1 ) ;
assume r [= q ; :: thesis: q in F
then p [= q by A4, LATTICES:25;
hence q in F ; :: thesis: verum

end;

hence { q where q is Element of : p [= q } is Filter of L by A1, Th9; :: thesis: verum