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