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