A1: for x, y being Element of L st x in DenseElements L & y in DenseElements L holds
x "\/" y in DenseElements L

proof

let x, y be Element of L; :: thesis: ( x in DenseElements L & y in DenseElements L implies x "\/" y in DenseElements L )
assume ( x in DenseElements L & y in DenseElements L ) ; :: thesis: x "\/" y in DenseElements L
then A2: ( x * = Bottom L & y * = Bottom L ) by DenseIsBot;
F1: (x "\/" y) * [= x * by Th6, LATTICES:5;
Bottom L [= (x "\/" y) * by LATTICES:16;
then (x "\/" y) * = Bottom L by LATTICES:8, A2, F1;
hence x "\/" y in DenseElements L ; :: thesis: verum

end;

for x, y being Element of L st x in DenseElements L & y in DenseElements L holds
x "/\" y in DenseElements L

proof

let x, y be Element of L; :: thesis: ( x in DenseElements L & y in DenseElements L implies x "/\" y in DenseElements L )
assume ( x in DenseElements L & y in DenseElements L ) ; :: thesis: x "/\" y in DenseElements L
then A2: ( x * = Bottom L & y * = Bottom L ) by DenseIsBot;
(x "/\" y) * = (x *) "\/" (y *) by Th12;
hence x "/\" y in DenseElements L by A2; :: thesis: verum

end;

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