let L be Stone Lattice; :: thesis: latt (L,(Skeleton L)) is complemented
set P = Skeleton L;
A0: ( Bottom L in Skeleton L & Top L in Skeleton L ) by Lm1;
set LL = latt (L,(Skeleton L));
for b being Element of (latt (L,(Skeleton L))) ex a being Element of (latt (L,(Skeleton L))) st a is_a_complement_of b

proof

let b be Element of (latt (L,(Skeleton L))); :: thesis: ex a being Element of (latt (L,(Skeleton L))) st a is_a_complement_of b
reconsider bb = b as Element of L by FILTER_2:68;
set aa = bb * ;
bb * in Skeleton L ;
then reconsider a = bb * as Element of (latt (L,(Skeleton L))) by FILTER_2:72;
b in the carrier of (latt (L,(Skeleton L))) ;
then z1: b in Skeleton L by FILTER_2:72;
(bb *) "\/" bb = (((bb *) *) *) "\/" bb by z1, Th13
.= (((bb *) *) *) "\/" ((bb *) *) by z1, Th13
.= Top L by SatStone ;
then A1: a "\/" b = Top L by FILTER_2:73
.= Top (latt (L,(Skeleton L))) by A0, ThC ;
(bb *) "/\" bb = Bottom L by ThD;
then a "/\" b = Bottom L by FILTER_2:73
.= Bottom (latt (L,(Skeleton L))) by A0, ThB ;
hence ex a being Element of (latt (L,(Skeleton L))) st a is_a_complement_of b by LATTICES:def 18, A1; :: thesis: verum

end;

hence latt (L,(Skeleton L)) is complemented by LATTICES:def 19; :: thesis: verum