take Trivial-Mem N ; :: thesis: ( Trivial-Mem N is IC-Ins-separated & Trivial-Mem N is with_non-empty_values & Trivial-Mem N is strict )
thus ( Trivial-Mem N is IC-Ins-separated & Trivial-Mem N is with_non-empty_values & Trivial-Mem N is strict ) ; :: thesis: verum