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) (O) B = X (O) B
let X, B be Subset of T; :: thesis: (X (O) B) (O) B = X (O) B
thus (X (O) B) (O) B c= X (O) B by Th41; :: according to XBOOLE_0:def 10 :: thesis: X (O) B c= (X (O) B) (O) B
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X (O) B or x in (X (O) B) (O) B )
assume x in X (O) B ; :: thesis: x in (X (O) B) (O) B
then consider x1, b1 being Point of T such that
A1: x = x1 + b1 and
A2: x1 in X (-) B and
A3: b1 in B ;
consider x2 being Point of T such that
A4: x1 = x2 and
A5: B + x2 c= X by A2;
(B + x2) (O) B c= X (O) B by A5, Th45;
then (B (O) B) + x2 c= X (O) B by Th46;
then B + x2 c= X (O) B by Th42;
then x1 in { x4 where x4 is Point of T : B + x4 c= X (O) B } by A4;
hence x in (X (O) B) (O) B by A1, A3; :: thesis: verum