theorem Th5: :: MIDSP_2:5

for S being non empty set
for a, b, c, d being Element of S
for G being non empty right_complementable add-associative right_zeroed addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G & w . (a,b) = w . (c,d) holds
w . (b,a) = w . (d,c)