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