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