theorem :: WEDDWITT:43

for R being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr
for a, b being Element of R st a in center R holds
a * b = b * a by Lm3;