theorem :: WEDDWITT:41

for R being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr
for x being Element of (center R) holds x is Element of R by Lm1;