let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for X, B, Y being Subset of T holds (X (-) B) \/ (Y (-) B) c= (X \/ Y) (-) B
let X, B, Y be Subset of T; :: thesis: (X (-) B) \/ (Y (-) B) c= (X \/ Y) (-) B
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (X (-) B) \/ (Y (-) B) or x in (X \/ Y) (-) B )
assume x in (X (-) B) \/ (Y (-) B) ; :: thesis: x in (X \/ Y) (-) B
then ( x in X (-) B or x in Y (-) B ) by XBOOLE_0:def 3;
then consider y being Point of T such that
A1: ( ( x = y & B + y c= X ) or ( x = y & B + y c= Y ) ) ;
B + y c= X \/ Y

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in B + y or z in X \/ Y )
assume z in B + y ; :: thesis: z in X \/ Y
hence z in X \/ Y by A1, XBOOLE_0:def 3; :: thesis: verum

end;

hence x in (X \/ Y) (-) B by A1; :: thesis: verum