let x be set ; :: thesis: for BL being non trivial B_Lattice holds
( x in StoneR BL iff ex a being Element of BL st (UFilter BL) . a = x )
let BL be non trivial B_Lattice; :: thesis: ( x in StoneR BL iff ex a being Element of BL st (UFilter BL) . a = x )
A1: ( x in StoneR BL implies ex a being Element of BL st (UFilter BL) . a = x )

proof

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

end;

( ex a being Element of BL st (UFilter BL) . a = x implies x in StoneR BL )

proof

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

end;

hence ( x in StoneR BL iff ex a being Element of BL st (UFilter BL) . a = x ) by A1; :: thesis: verum