let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for X, B being Subset of T holds X c= (X (+) B) (-) B
let X, B be Subset of T; :: thesis: X c= (X (+) B) (-) B
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in (X (+) B) (-) B )
assume A1: x in X ; :: thesis: x in (X (+) B) (-) B
then consider x1 being Point of T such that
A2: x1 = x ;
B + x1 c= B (+) X by A1, A2, Th19;
then x in (B (+) X) (-) B by A2;
hence x in (X (+) B) (-) B by Th12; :: thesis: verum