let L be D_Lattice; :: thesis: for a, b being Element of L st a <> b holds
(StoneH L) . a <> (StoneH L) . b
let a, b be Element of L; :: thesis: ( a <> b implies (StoneH L) . a <> (StoneH L) . b )
assume a <> b ; :: thesis: (StoneH L) . a <> (StoneH L) . b
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;
then consider F being Filter of L such that
A1: F in F_primeSet L and
A2: ( ( b in F & not a in F ) or ( a in F & not b in F ) ) ;
( ( F in (StoneH L) . a & not F in (StoneH L) . b ) or ( F in (StoneH L) . b & not F in (StoneH L) . a ) ) by A1, A2, Th11;
hence (StoneH L) . a <> (StoneH L) . b ; :: thesis: verum