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