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