take {(Top L)} ; :: thesis: ( not {(Top L)} is empty & {(Top L)} is finite & {(Top L)} is countable & {(Top L)} is dense )
thus ( not {(Top L)} is empty & {(Top L)} is finite & {(Top L)} is countable ) ; :: thesis: {(Top L)} is dense
thus {(Top L)} is dense by Th38; :: thesis: verum