let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for X, B being Subset of T
for x being Point of T st x in X holds
B + x c= B (+) X
let X, B be Subset of T; :: thesis: for x being Point of T st x in X holds
B + x c= B (+) X
let x be Point of T; :: thesis: ( x in X implies B + x c= B (+) X )
assume A1: x in X ; :: thesis: B + x c= B (+) X
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in B + x or y in B (+) X )
assume y in B + x ; :: thesis: y in B (+) X
then ex y1 being Point of T st
( y = y1 + x & y1 in B ) ;
hence y in B (+) X by A1; :: thesis: verum