let L be distributive bounded pseudocomplemented Lattice; :: thesis: ( L is satisfying_Stone_identity iff for a, b being Element of L holds (a "/\" b) * = (a *) "\/" (b *) )

hereby :: thesis: ( ( for a, b being Element of L holds (a "/\" b) * = (a *) "\/" (b *) ) implies L is satisfying_Stone_identity )

assume a11: L is satisfying_Stone_identity ; :: thesis: for a, b being Element of L holds (a "/\" b) * = (a *) "\/" (b *)
let a, b be Element of L; :: thesis: (a "/\" b) * = (a *) "\/" (b *)
set g = a "/\" b;
a0: (a "/\" b) "/\" ((a *) "\/" (b *)) = ((a *) "/\" (a "/\" b)) "\/" ((a "/\" b) "/\" (b *)) by LATTICES:def 11
.= (((a *) "/\" a) "/\" b) "\/" ((a "/\" b) "/\" (b *)) by LATTICES:def 7
.= (((a *) "/\" a) "/\" b) "\/" (a "/\" (b "/\" (b *))) by LATTICES:def 7
.= ((Bottom L) "/\" b) "\/" (a "/\" (b "/\" (b *))) by ThD
.= ((Bottom L) "/\" b) "\/" (a "/\" (Bottom L)) by ThD
.= Bottom L ;
for x being Element of L st (a "/\" b) "/\" x = Bottom L holds
x [= (a *) "\/" (b *)

proof

let x be Element of L; :: thesis: ( (a "/\" b) "/\" x = Bottom L implies x [= (a *) "\/" (b *) )
set z = b "/\" x;
set w = x "/\" ((a *) *);
assume a1: (a "/\" b) "/\" x = Bottom L ; :: thesis: x [= (a *) "\/" (b *)
a0: Bottom L [= (b "/\" x) "/\" ((a *) *) by LATTICES:16;
a2: (b "/\" x) "/\" a = Bottom L by a1, LATTICES:def 7;
a * is_a_pseudocomplement_of a by def3;
then (b "/\" x) "/\" ((a *) *) [= (a *) "/\" ((a *) *) by LATTICES:9, a2;
then (b "/\" x) "/\" ((a *) *) [= Bottom L by ThD;
then (b "/\" x) "/\" ((a *) *) = Bottom L by LATTICES:8, a0;
then a4: (x "/\" ((a *) *)) "/\" b = Bottom L by LATTICES:def 7;
b * is_a_pseudocomplement_of b by def3;
then a5: x "/\" ((a *) *) [= b * by a4;
a6: x "/\" (a *) [= a * by LATTICES:6;
x = x "/\" (Top L)
.= x "/\" ((a *) "\/" ((a *) *)) by a11
.= (x "/\" (a *)) "\/" (x "/\" ((a *) *)) by LATTICES:def 11 ;
hence x [= (a *) "\/" (b *) by a5, a6, FILTER_0:4; :: thesis: verum

end;

then (a *) "\/" (b *) is_a_pseudocomplement_of a "/\" b by a0;
hence (a "/\" b) * = (a *) "\/" (b *) by def3; :: thesis: verum

end;

assume a1: for a, b being Element of L holds (a "/\" b) * = (a *) "\/" (b *) ; :: thesis: L is satisfying_Stone_identity
let x be Element of L; :: according to LATSTONE:def 5 :: thesis: (x *) "\/" ((x *) *) = Top L
x "/\" (x *) = Bottom L by ThD;
then (x *) "\/" ((x *) *) = (Bottom L) * by a1;
hence (x *) "\/" ((x *) *) = Top L by Th11; :: thesis: verum