let L be distributive Lattice; :: thesis: for x being set holds
( x in StoneR L iff ex a being Element of L st (PrimeFilters L) . a = x )
let x be set ; :: thesis: ( x in StoneR L iff ex a being Element of L st (PrimeFilters L) . a = x )
thus ( x in StoneR L implies ex a being Element of L st (PrimeFilters L) . a = x ) :: thesis: ( ex a being Element of L st (PrimeFilters L) . a = x implies x in StoneR L )

proof

assume x in StoneR L ; :: thesis: ex a being Element of L st (PrimeFilters L) . a = x
then consider y being object such that
A2: y in dom (PrimeFilters L) and
A3: x = (PrimeFilters L) . y by FUNCT_1:def 3;
reconsider a = y as Element of L by A2;
take a ; :: thesis: (PrimeFilters L) . a = x
thus (PrimeFilters L) . a = x by A3; :: thesis: verum

end;

given a being Element of L such that A4: x = (PrimeFilters L) . a ; :: thesis: x in StoneR L
a in the carrier of L ;
then a in dom (PrimeFilters L) by Def6;
hence x in StoneR L by A4, FUNCT_1:def 3; :: thesis: verum