take Trivial-COM N ; :: thesis: Trivial-COM N is standard-ins
thus Trivial-COM N is standard-ins ; :: thesis: verum