take Trivial-Mem N ; :: thesis: Trivial-Mem N is 1 -element
thus Trivial-Mem N is 1 -element ; :: thesis: verum