theorem :: MATHMORP:40

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B being Subset of T holds ((X `) (o) (B !)) ` = X (O) B