take Trivial-addMagma ; :: thesis: ( Trivial-addMagma is add-cancelable & Trivial-addMagma is strict & not Trivial-addMagma is empty & Trivial-addMagma is trivial )
thus ( Trivial-addMagma is add-cancelable & Trivial-addMagma is strict & not Trivial-addMagma is empty & Trivial-addMagma is trivial ) ; :: thesis: verum