let L be Lattice; :: thesis: for a being Element of L holds { F where F is Filter of L : ( F is prime & a in F ) } c= PFilters L
let a be Element of L; :: thesis: { F where F is Filter of L : ( F is prime & a in F ) } c= PFilters L
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F where F is Filter of L : ( F is prime & a in F ) } or x in PFilters L )
assume x in { F where F is Filter of L : ( F is prime & a in F ) } ; :: thesis: x in PFilters L
then ex UF being Filter of L st
( UF = x & UF is prime & a in UF ) ;
hence x in PFilters L ; :: thesis: verum