take Trivial-addMagma ; :: thesis: ( Trivial-addMagma is strict & Trivial-addMagma is 1 -element )
thus ( Trivial-addMagma is strict & Trivial-addMagma is 1 -element ) ; :: thesis: verum