let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for X, B being Subset of T holds ((X `) (O) (B !)) ` = X (o) B
let X, B be Subset of T; :: thesis: ((X `) (O) (B !)) ` = X (o) B
((X `) (O) (B !)) ` = (((((X `) (-) (B !)) `) (-) B) `) ` by Th37
.= (X (+) ((B !) !)) (-) B by Th37
.= (X (+) B) (-) B by Th1 ;
hence ((X `) (O) (B !)) ` = X (o) B ; :: thesis: verum