take Trivial-addLoopStr ; :: thesis: ( Trivial-addLoopStr is strict & Trivial-addLoopStr is left_zeroed & Trivial-addLoopStr is right_zeroed & Trivial-addLoopStr is Loop-like )
thus ( Trivial-addLoopStr is strict & Trivial-addLoopStr is left_zeroed & Trivial-addLoopStr is right_zeroed & Trivial-addLoopStr is Loop-like ) ; :: thesis: verum