:: deftheorem defines F_primeSet OPENLATT:def 5 :
for L being D_Lattice holds F_primeSet L = { F where F is Filter of L : ( F <> the carrier of L & F is prime ) } ;