take Trivial-COM N ; :: thesis: ( Trivial-COM N is proper-halt & Trivial-COM N is regular & Trivial-COM N is homogeneous & Trivial-COM N is J/A-independent & Trivial-COM N is realistic & Trivial-COM N is IC-Ins-separated & Trivial-COM N is definite )
thus ( Trivial-COM N is proper-halt & Trivial-COM N is regular & Trivial-COM N is homogeneous & Trivial-COM N is J/A-independent & Trivial-COM N is realistic & Trivial-COM N is IC-Ins-separated & Trivial-COM N is definite ) ; :: thesis: verum