let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for X, Y, B being Subset of T holds (B (-) X) \/ (B (-) Y) c= B (-) (X /\ Y)
let X, Y, B be Subset of T; :: thesis: (B (-) X) \/ (B (-) Y) c= B (-) (X /\ Y)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (B (-) X) \/ (B (-) Y) or x in B (-) (X /\ Y) )
assume x in (B (-) X) \/ (B (-) Y) ; :: thesis: x in B (-) (X /\ Y)
then ( x in B (-) X or x in B (-) Y ) by XBOOLE_0:def 3;
then consider y being Point of T such that
A1: ( ( x = y & X + y c= B ) or ( x = y & Y + y c= B ) ) ;
(X + y) /\ (Y + y) c= B
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (X + y) /\ (Y + y) or a in B )
assume A2: a in (X + y) /\ (Y + y) ; :: thesis: a in B
then A3: a in X + y by XBOOLE_0:def 4;
A4: a in Y + y by A2, XBOOLE_0:def 4;
per cases ( X + y c= B or Y + y c= B ) by A1;
suppose X + y c= B ; :: thesis: a in B
hence a in B by A3; :: thesis: verum
end;
suppose Y + y c= B ; :: thesis: a in B
hence a in B by A4; :: thesis: verum
end;
end;
end;
then (X /\ Y) + y c= B by Th28;
hence x in B (-) (X /\ Y) by A1; :: thesis: verum