take Top L ; :: thesis: Top L is dense
thus Top L is dense ; :: thesis: verum