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