let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for x being Point of T
for X being Subset of T st X = {} holds
X + x = {}
let x be Point of T; :: thesis: for X being Subset of T st X = {} holds
X + x = {}
let X be Subset of T; :: thesis: ( X = {} implies X + x = {} )
assume A1: X = {} ; :: thesis: X + x = {}
now :: thesis: for y being object holds not y in X + x
given y being object such that A2: y in X + x ; :: thesis: contradiction
ex y1 being Point of T st
( y = y1 + x & y1 in X ) by A2;
hence contradiction by A1; :: thesis: verum
end;
hence X + x = {} by XBOOLE_0:def 1; :: thesis: verum