take
Trivial-AMI N
; :: thesis: ( Trivial-AMI N is IC-Ins-separated & Trivial-AMI N is halting & Trivial-AMI N is strict )

thus ( Trivial-AMI N is IC-Ins-separated & Trivial-AMI N is halting & Trivial-AMI N is strict ) ; :: thesis: verum

thus ( Trivial-AMI N is IC-Ins-separated & Trivial-AMI N is halting & Trivial-AMI N is strict ) ; :: thesis: verum