let L be Lattice; :: thesis: for F being Filter of L
for a being Element of L
for G being set st G = { x where x is Element of L : ex u being Element of L st
( u in F & a "/\" u [= x ) } & a in G holds
G is Filter of L
let F be Filter of L; :: thesis: for a being Element of L
for G being set st G = { x where x is Element of L : ex u being Element of L st
( u in F & a "/\" u [= x ) } & a in G holds
G is Filter of L
let a be Element of L; :: thesis: for G being set st G = { x where x is Element of L : ex u being Element of L st
( u in F & a "/\" u [= x ) } & a in G holds
G is Filter of L
let G be set ; :: thesis: ( G = { x where x is Element of L : ex u being Element of L st
( u in F & a "/\" u [= x ) } & a in G implies G is Filter of L )
assume A1: ( G = { x where x is Element of L : ex u being Element of L st
( u in F & a "/\" u [= x ) } & a in G ) ; :: thesis: G is Filter of L
G c= the carrier of L

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in G or y in the carrier of L )
assume y in G ; :: thesis: y in the carrier of L
then consider x being Element of L such that
S2: ( y = x & ex u being Element of L st
( u in F & a "/\" u [= x ) ) by A1;
thus y in the carrier of L by S2; :: thesis: verum

end;

then reconsider G1 = G as Subset of L ;
set u = the Element of F;
ZD: G1 is meet-closed

proof

let p, q be Element of L; :: according to LATTICES:def 24 :: thesis: ( not p in G1 or not q in G1 or p "/\" q in G1 )
assume P0: ( p in G1 & q in G1 ) ; :: thesis: p "/\" q in G1
then consider xx being Element of L such that
P1: ( xx = p & ex u being Element of L st
( u in F & a "/\" u [= xx ) ) by A1;
consider u1 being Element of L such that
P3: ( u1 in F & a "/\" u1 [= p ) by P1;
consider yy being Element of L such that
P2: ( yy = q & ex u being Element of L st
( u in F & a "/\" u [= yy ) ) by P0, A1;
consider u2 being Element of L such that
P4: ( u2 in F & a "/\" u2 [= q ) by P2;
P6: (a "/\" u1) "/\" (a "/\" u2) [= p "/\" q by P3, P4, FILTER_0:5;
P7: u1 "/\" u2 in F by P3, P4, FILTER_0:8;
(a "/\" u1) "/\" (a "/\" u2) = ((a "/\" u1) "/\" a) "/\" u2 by LATTICES:def 7
.= ((a "/\" a) "/\" u1) "/\" u2 by LATTICES:def 7
.= a "/\" (u1 "/\" u2) by LATTICES:def 7 ;
hence p "/\" q in G1 by P7, P6, A1; :: thesis: verum

end;

G1 is final

proof

let p, q be Element of L; :: according to LATTICES:def 23 :: thesis: ( not p [= q or not p in G1 or q in G1 )
assume Y0: ( p [= q & p in G1 ) ; :: thesis: q in G1
then consider s being Element of L such that
Y1: ( s = p & ex u being Element of L st
( u in F & a "/\" u [= s ) ) by A1;
consider u being Element of L such that
Y2: ( u in F & a "/\" u [= s ) by Y1;
a "/\" u [= q by Y2, Y0, Y1, LATTICES:7;
hence q in G1 by Y2, A1; :: thesis: verum

end;

hence G is Filter of L by A1, ZD; :: thesis: verum