set S = Skeleton L;
tt: for p, q being Element of L st p in Skeleton L & q in Skeleton L holds
p "\/" q in Skeleton L

proof

let p, q be Element of L; :: thesis: ( p in Skeleton L & q in Skeleton L implies p "\/" q in Skeleton L )
assume ( p in Skeleton L & q in Skeleton L ) ; :: thesis: p "\/" q in Skeleton L
then ( (p *) * = p & (q *) * = q ) by Th13;
then p "\/" q = ((p *) "/\" (q *)) * by Th12;
hence p "\/" q in Skeleton L ; :: thesis: verum

end;

for p, q being Element of L st p in Skeleton L & q in Skeleton L holds
p "/\" q in Skeleton L

proof

let p, q be Element of L; :: thesis: ( p in Skeleton L & q in Skeleton L implies p "/\" q in Skeleton L )
assume T1: ( p in Skeleton L & q in Skeleton L ) ; :: thesis: p "/\" q in Skeleton L
then T3: p = (p *) * by Th13;
p * [= (p "/\" q) * by Th6, LATTICES:6;
then T2: ((p "/\" q) *) * [= (p *) * by Th6;
T4: q = (q *) * by T1, Th13;
q * [= (p "/\" q) * by Th6, LATTICES:6;
then ((p "/\" q) *) * [= (q *) * by Th6;
then T5: ((p "/\" q) *) * [= p "/\" q by T3, T4, T2, FILTER_0:7;
p "/\" q [= ((p "/\" q) *) * by Th5;
then p "/\" q = ((p "/\" q) *) * by T5, LATTICES:8;
hence p "/\" q in Skeleton L ; :: thesis: verum

end;

hence ( Skeleton L is join-closed & Skeleton L is meet-closed ) by tt, LATTICES:def 24, LATTICES:def 25; :: thesis: verum