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