take Trivial-COM ; :: thesis: ( Trivial-COM is regular & Trivial-COM is J/A-independent & Trivial-COM is homogeneous )
thus ( Trivial-COM is regular & Trivial-COM is J/A-independent & Trivial-COM is homogeneous ) ; :: thesis: verum