let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for X, B, C being Subset of T holds X (-) (B \/ C) = (X (-) B) /\ (X (-) C)
let X, B, C be Subset of T; :: thesis: X (-) (B \/ C) = (X (-) B) /\ (X (-) C)
thus X (-) (B \/ C) c= (X (-) B) /\ (X (-) C) :: according to XBOOLE_0:def 10 :: thesis: (X (-) B) /\ (X (-) C) c= X (-) (B \/ C)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X (-) (B \/ C) or x in (X (-) B) /\ (X (-) C) )
assume x in X (-) (B \/ C) ; :: thesis: x in (X (-) B) /\ (X (-) C)
then consider y being Point of T such that
A1: x = y and
A2: (B \/ C) + y c= X ;
A3: (B + y) \/ (C + y) c= X by A2, Th27;
then C + y c= X by XBOOLE_1:11;
then A4: x in { y1 where y1 is Point of T : C + y1 c= X } by A1;
B + y c= X by A3, XBOOLE_1:11;
then x in { y1 where y1 is Point of T : B + y1 c= X } by A1;
hence x in (X (-) B) /\ (X (-) C) by A4, XBOOLE_0:def 4; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (X (-) B) /\ (X (-) C) or x in X (-) (B \/ C) )
assume A5: x in (X (-) B) /\ (X (-) C) ; :: thesis: x in X (-) (B \/ C)
then x in X (-) B by XBOOLE_0:def 4;
then consider y being Point of T such that
A6: x = y and
A7: B + y c= X ;
x in X (-) C by A5, XBOOLE_0:def 4;
then ex y2 being Point of T st
( x = y2 & C + y2 c= X ) ;
then (B + y) \/ (C + y) c= X by A6, A7, XBOOLE_1:8;
then (B \/ C) + y c= X by Th27;
hence x in X (-) (B \/ C) by A6; :: thesis: verum