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

hereby :: thesis: ( ( for a, b being Element of L st a in Skeleton L & b in Skeleton L holds
a "\/" b in Skeleton L ) implies L is satisfying_Stone_identity )

assume a0: L is satisfying_Stone_identity ; :: thesis: for a, b being Element of L st a in Skeleton L & b in Skeleton L holds
a "\/" b in Skeleton L
let a, b be Element of L; :: thesis: ( a in Skeleton L & b in Skeleton L implies a "\/" b in Skeleton L )
assume X0: ( a in Skeleton L & b in Skeleton L ) ; :: thesis: a "\/" b in Skeleton L
then consider x being Element of L such that
X1: a = x * ;
consider y being Element of L such that
X2: b = y * by X0;
(x "/\" y) * in Skeleton L ;
hence a "\/" b in Skeleton L by X1, X2, Th12, a0; :: thesis: verum

end;

assume a1: for a, b being Element of L st a in Skeleton L & b in Skeleton L holds
a "\/" b in Skeleton L ; :: thesis: L is satisfying_Stone_identity
let y be Element of L; :: according to LATSTONE:def 5 :: thesis: (y *) "\/" ((y *) *) = Top L
( y * in Skeleton L & (y *) * in Skeleton L ) ;
then sp: (((y *) "\/" ((y *) *)) *) * = (y *) "\/" ((y *) *) by Th13, a1;
r1: (y *) * [= ((y *) "/\" ((y *) *)) * by Th6, LATTICES:6;
((y *) *) * [= ((y *) "/\" ((y *) *)) * by LATTICES:6, Th6;
then y * [= ((y *) "/\" ((y *) *)) * by Th7;
then r: (y *) "\/" ((y *) *) [= (((y *) "/\" ((y *) *)) *) "\/" (((y *) "/\" ((y *) *)) *) by r1, FILTER_0:4;
s1: ((y *) "\/" ((y *) *)) * [= (y *) * by Th6, LATTICES:5;
((y *) "\/" ((y *) *)) * [= ((y *) *) * by Th6, LATTICES:5;
then s2: ((y *) "\/" ((y *) *)) * [= y * by Th7;
(((y *) "\/" ((y *) *)) *) "/\" (((y *) "\/" ((y *) *)) *) [= (y *) "/\" ((y *) *) by s1, s2, FILTER_0:5;
then ((y *) "/\" ((y *) *)) * [= (y *) "\/" ((y *) *) by sp, Th6;
then ((y *) "/\" ((y *) *)) * = (y *) "\/" ((y *) *) by r, LATTICES:8;
then (Bottom L) * = (y *) "\/" ((y *) *) by ThD;
hence (y *) "\/" ((y *) *) = Top L by Th11; :: thesis: verum