take Trivial-COM N ; :: thesis: ( Trivial-COM N is IC-Ins-separated & Trivial-COM N is definite & Trivial-COM N is standard-ins )
thus ( Trivial-COM N is IC-Ins-separated & Trivial-COM N is definite & Trivial-COM N is standard-ins ) ; :: thesis: verum