take Trivial-AMI IL,N ; :: thesis: ( Trivial-AMI IL,N is IC-Ins-separated & Trivial-AMI IL,N is halting & Trivial-AMI IL,N is steady-programmed & Trivial-AMI IL,N is definite & Trivial-AMI IL,N is strict )
thus ( Trivial-AMI IL,N is IC-Ins-separated & Trivial-AMI IL,N is halting & Trivial-AMI IL,N is steady-programmed & Trivial-AMI IL,N is definite & Trivial-AMI IL,N is strict ) ; :: thesis: verum