theorem Th6: :: BASEL_2:6

for L being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive commutative doubleLoopStr holds <%(0. L),(0. L),(1. L)%> = <%(0. L),(1. L)%> `^ 2