:: deftheorem defines maximal LATTICEA:def 3 :
for L being Lattice
for F being Filter of L holds
( F is maximal iff ( F is proper & ( for G being Filter of L st G is proper & F c= G holds
F = G ) ) );