take Trivial-COM ; :: thesis: ( Trivial-COM is standard-ins & Trivial-COM is strict )
thus ( Trivial-COM is standard-ins & Trivial-COM is strict ) ; :: thesis: verum