take latt (L, the non empty ClosedSubset of L) ; :: thesis: not latt (L, the non empty ClosedSubset of L) is empty
thus not latt (L, the non empty ClosedSubset of L) is empty ; :: thesis: verum