let X be non empty set ; :: thesis: for F being non empty Subset of (BooleLatt X) holds
( F is Filter of (BooleLatt X) iff ( ( for p, q being Element of F holds p /\ q in F ) & ( for p being Element of F
for q being Element of (BooleLatt X) st p c= q holds
q in F ) ) )
let F be non empty Subset of (BooleLatt X); :: thesis: ( F is Filter of (BooleLatt X) iff ( ( for p, q being Element of F holds p /\ q in F ) & ( for p being Element of F
for q being Element of (BooleLatt X) st p c= q holds
q in F ) ) )

hereby :: thesis: ( ( for p, q being Element of F holds p /\ q in F ) & ( for p being Element of F
for q being Element of (BooleLatt X) st p c= q holds
q in F ) implies F is Filter of (BooleLatt X) )

assume A1: F is Filter of (BooleLatt X) ; :: thesis: ( ( for p, q being Element of F holds p /\ q in F ) & ( for p being Element of F
for q being Element of (BooleLatt X) st p c= q holds
q in F ) )
then A2: for p, q being Element of (BooleLatt X) st p in F & p [= q holds
q in F by FILTER_0:9;

now :: thesis: for p, q being Element of (BooleLatt X) holds
( ( p in F & q in F implies p /\ q in F ) & ( p in F & p c= q implies q in F ) )

let p, q be Element of (BooleLatt X); :: thesis: ( ( p in F & q in F implies p /\ q in F ) & ( p in F & p c= q implies q in F ) )

now :: thesis: ( p in F & q in F implies p /\ q in F )

assume ( p in F & q in F ) ; :: thesis: p /\ q in F
then p "/\" q in F by A1, FILTER_0:9;
hence p /\ q in F ; :: thesis: verum

end;

hence ( ( p in F & q in F implies p /\ q in F ) & ( p in F & p c= q implies q in F ) ) by A2, LATTICE3:2; :: thesis: verum

end;

hence ( ( for p, q being Element of F holds p /\ q in F ) & ( for p being Element of F
for q being Element of (BooleLatt X) st p c= q holds
q in F ) ) ; :: thesis: verum

end;

assume that
A3: for p, q being Element of F holds p /\ q in F and
A4: for p being Element of F
for q being Element of (BooleLatt X) st p c= q holds
q in F ; :: thesis: F is Filter of (BooleLatt X)
A5: for p, q being Element of (BooleLatt X) st p in F & q in F holds
p "/\" q in F by A3;
for p, q being Element of (BooleLatt X) st p in F & p [= q holds
q in F by A4, LATTICE3:2;
hence F is Filter of (BooleLatt X) by A5, FILTER_0:9; :: thesis: verum