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