let L be D_Lattice; :: thesis: for a, b being Element of L st a <> b holds
ex F being Filter of L st F in F_primeSet L
let a, b be Element of L; :: thesis: ( a <> b implies ex F being Filter of L st F in F_primeSet L )
assume a <> b ; :: thesis: ex F being Filter of L st F in F_primeSet L
then ( not a [= b or not b [= a ) by LATTICES:8;
then ( ex F being Filter of L st
( F in F_primeSet L & not b in F & a in F ) or ex F being Filter of L st
( F in F_primeSet L & not a in F & b in F ) ) by Th20;
hence ex F being Filter of L st F in F_primeSet L ; :: thesis: verum