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 ; :: thesis: verum
end;
hence ( x in StoneR BL iff ex a being Element of BL st (UFilter BL) . a = x ) by A1; :: thesis: verum