take { the set } ; :: thesis: not { the set } is empty
thus not { the set } is empty ; :: thesis: verum