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 Th38
.= (((X `) (+) (B !)) `) (+) B by Th1
.= (((X (-) B) `) `) (+) B by Th38 ;
hence ((X `) (o) (B !)) ` = X (O) B ; :: thesis: verum