let L be D_Lattice; :: thesis: StoneH L is one-to-one
let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in dom (StoneH L) or not x2 in dom (StoneH L) or not (StoneH L) . x1 = (StoneH L) . x2 or x1 = x2 )
assume that
A1: ( x1 in dom (StoneH L) & x2 in dom (StoneH L) ) and
A2: (StoneH L) . x1 = (StoneH L) . x2 ; :: thesis: x1 = x2
reconsider a1 = x1, a2 = x2 as Element of L by A1, Def6;
a1 = a2 by A2, Th24;
hence x1 = x2 ; :: thesis: verum