take Trivial-AMI IL,N ; :: thesis: ( Trivial-AMI IL,N is standard-ins & not Trivial-AMI IL,N is empty & Trivial-AMI IL,N is stored-program )
thus ( Trivial-AMI IL,N is standard-ins & not Trivial-AMI IL,N is empty & Trivial-AMI IL,N is stored-program ) ; :: thesis: verum