let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for X, Y being Subset of T st Y = {} holds
X (-) Y = the carrier of T
let X, Y be Subset of T; :: thesis: ( Y = {} implies X (-) Y = the carrier of T )
assume A1: Y = {} ; :: thesis: X (-) Y = the carrier of T
{ y where y is Point of T : Y + y c= X } = the carrier of T

proof

thus { y where y is Point of T : Y + y c= X } c= the carrier of T :: according to XBOOLE_0:def 10 :: thesis: the carrier of T c= { y where y is Point of T : Y + y c= X }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { y where y is Point of T : Y + y c= X } or x in the carrier of T )
assume x in { y where y is Point of T : Y + y c= X } ; :: thesis: x in the carrier of T
then ex y being Point of T st
( x = y & Y + y c= X ) ;
hence x in the carrier of T ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of T or x in { y where y is Point of T : Y + y c= X } )
assume x in the carrier of T ; :: thesis: x in { y where y is Point of T : Y + y c= X }
then reconsider a = x as Point of T ;
Y + a = {} by A1, Th4;
then Y + a c= X ;
hence x in { y where y is Point of T : Y + y c= X } ; :: thesis: verum

end;

hence X (-) Y = the carrier of T ; :: thesis: verum