take CAlgebra {0} ; :: thesis: ( CAlgebra {0} is strict & CAlgebra {0} is Abelian & CAlgebra {0} is add-associative & CAlgebra {0} is right_zeroed & CAlgebra {0} is right_complementable & CAlgebra {0} is commutative & CAlgebra {0} is associative & CAlgebra {0} is right_unital & CAlgebra {0} is right-distributive & CAlgebra {0} is vector-distributive & CAlgebra {0} is scalar-distributive & CAlgebra {0} is scalar-associative & CAlgebra {0} is vector-associative )
thus ( CAlgebra {0} is strict & CAlgebra {0} is Abelian & CAlgebra {0} is add-associative & CAlgebra {0} is right_zeroed & CAlgebra {0} is right_complementable & CAlgebra {0} is commutative & CAlgebra {0} is associative & CAlgebra {0} is right_unital & CAlgebra {0} is right-distributive & CAlgebra {0} is vector-distributive & CAlgebra {0} is scalar-distributive & CAlgebra {0} is scalar-associative & CAlgebra {0} is vector-associative ) ; :: thesis: verum