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