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

(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