take Trivial-Mem N ; :: thesis: Trivial-Mem N is with_non-empty_values
thus Trivial-Mem N is with_non-empty_values ; :: thesis: verum