let L be Boolean Lattice; :: thesis: L is satisfying_Stone_identity
let x be Element of L; :: according to LATSTONE:def 5 :: thesis: (x *) "\/" ((x *) *) = Top L
(x *) "\/" ((x *) *) = Top L

proof

(x *) "\/" ((x *) *) = (x `) "\/" ((x *) *) by ThE
.= (x `) "\/" ((x `) *) by ThE
.= (x `) "\/" ((x `) `) by ThE
.= Top L by LATTICES:21 ;
hence (x *) "\/" ((x *) *) = Top L ; :: thesis: verum

end;

hence (x *) "\/" ((x *) *) = Top L ; :: thesis: verum