take S = Trivial-addLoopStr ; :: thesis: ( S is strict & S is Abelian & S is add-associative & S is right_zeroed & S is right_complementable & not S is empty )
thus S is strict ; :: thesis: ( S is Abelian & S is add-associative & S is right_zeroed & S is right_complementable & not S is empty )
thus S is Abelian by STRUCT_0:def 10; :: thesis: ( S is add-associative & S is right_zeroed & S is right_complementable & not S is empty )
thus S is add-associative by STRUCT_0:def 10; :: thesis: ( S is right_zeroed & S is right_complementable & not S is empty )
thus S is right_zeroed by STRUCT_0:def 10; :: thesis: ( S is right_complementable & not S is empty )
thus ( S is right_complementable & not S is empty ) ; :: thesis: verum