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