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