take
Trivial-AMI M
; :: thesis: ( Trivial-AMI M is IC-Ins-separated & Trivial-AMI M is strict & Trivial-AMI M is trivial )

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

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