let L be Stone Lattice; :: thesis: for a being Element of L ex b, c being Element of L st
( a = b "/\" c & b in Skeleton L & c in DenseElements L )
let a be Element of L; :: thesis: ex b, c being Element of L st
( a = b "/\" c & b in Skeleton L & c in DenseElements L )
A1: a = (((a *) *) "/\" a) "\/" (Bottom L) by LATTICES:4, Th5
.= (((a *) *) "/\" a) "\/" (((a *) *) "/\" (a *)) by ThD
.= ((a *) *) "/\" (a "\/" (a *)) by LATTICES:def 11 ;
take b = (a *) * ; :: thesis: ex c being Element of L st
( a = b "/\" c & b in Skeleton L & c in DenseElements L )
take c = a "\/" (a *); :: thesis: ( a = b "/\" c & b in Skeleton L & c in DenseElements L )
G1: (a "\/" (a *)) * [= a * by Th6, LATTICES:5;
(a "\/" (a *)) * [= (a *) * by Th6, LATTICES:5;
then (a "\/" (a *)) * [= (a *) "/\" ((a *) *) by FILTER_0:7, G1;
then (a "\/" (a *)) * [= Bottom L by ThD;
then (a "\/" (a *)) * = Bottom L by BOOLEALG:9;
hence ( a = b "/\" c & b in Skeleton L & c in DenseElements L ) by A1; :: thesis: verum