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 )

( 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

( ex a being Element of BL st (UFilter BL) . a = x implies x in StoneR BL )
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;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

proof

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