let L be D_Lattice; :: thesis: for x being set holds
( x in StoneS L iff ex a being Element of L st x = (StoneH L) . a )
let x be set ; :: thesis: ( x in StoneS L iff ex a being Element of L st x = (StoneH L) . a )

hereby :: thesis: ( ex a being Element of L st x = (StoneH L) . a implies x in StoneS L )

assume x in StoneS L ; :: thesis: ex y being Element of L st x = (StoneH L) . y
then consider y being object such that
A1: y in dom (StoneH L) and
A2: x = (StoneH L) . y by FUNCT_1:def 3;
reconsider y = y as Element of L by A1, Def6;
take y = y; :: thesis: x = (StoneH L) . y
thus x = (StoneH L) . y by A2; :: thesis: verum

end;

given b being Element of L such that A3: x = (StoneH L) . b ; :: thesis: x in StoneS L
b in the carrier of L ;
then b in dom (StoneH L) by Def6;
hence x in StoneS L by A3, FUNCT_1:def 3; :: thesis: verum