take Trivial-AMI N ; :: thesis: ( Trivial-AMI N is IC-Ins-separated & Trivial-AMI N is standard-ins )
thus ( Trivial-AMI N is IC-Ins-separated & Trivial-AMI N is standard-ins ) ; :: thesis: verum