let E be RealLinearSpace; :: thesis: for A, B being non empty binary-image of E holds
( ( the carrier of E \ A) (+) B = the carrier of E \ (A (-) B) & ( the carrier of E \ A) (-) B = the carrier of E \ (A (+) B) )
let A, B be non empty binary-image of E; :: thesis: ( ( the carrier of E \ A) (+) B = the carrier of E \ (A (-) B) & ( the carrier of E \ A) (-) B = the carrier of E \ (A (+) B) )

per cases ( A = the carrier of E or A <> the carrier of E ) ;

suppose X0: A = the carrier of E ; :: thesis: ( ( the carrier of E \ A) (+) B = the carrier of E \ (A (-) B) & ( the carrier of E \ A) (-) B = the carrier of E \ (A (+) B) )

reconsider X = {} as Subset of E by XBOOLE_1:2;
thus ( the carrier of E \ A) (+) B = X (+) B by X0, XBOOLE_1:37
.= {} by LM0010
.= the carrier of E \ the carrier of E by XBOOLE_1:37
.= the carrier of E \ (A (-) B) by X0, LM0020A ; :: thesis: ( the carrier of E \ A) (-) B = the carrier of E \ (A (+) B)
thus ( the carrier of E \ A) (-) B = X (-) B by X0, XBOOLE_1:37
.= {} by LM0010A
.= the carrier of E \ the carrier of E by XBOOLE_1:37
.= the carrier of E \ (A (+) B) by X0, LM0020 ; :: thesis: verum

end;

suppose X0: A <> the carrier of E ; :: thesis: ( ( the carrier of E \ A) (+) B = the carrier of E \ (A (-) B) & ( the carrier of E \ A) (-) B = the carrier of E \ (A (+) B) )

P1: not the carrier of E \ A is empty

proof

assume the carrier of E \ A is empty ; :: thesis: contradiction
then the carrier of E c= A by XBOOLE_1:37;
hence contradiction by X0, XBOOLE_0:def 10; :: thesis: verum

end;

X1: for x being set holds
( x in { v where v is Element of E : (v + ((- 1) * B)) /\ ( the carrier of E \ A) <> {} } iff ( x in the carrier of E & not x in { v where v is Element of E : v + ((- 1) * B) c= A } ) )

proof

let x be set ; :: thesis: ( x in { v where v is Element of E : (v + ((- 1) * B)) /\ ( the carrier of E \ A) <> {} } iff ( x in the carrier of E & not x in { v where v is Element of E : v + ((- 1) * B) c= A } ) )

hereby :: thesis: ( x in the carrier of E & not x in { v where v is Element of E : v + ((- 1) * B) c= A } implies x in { v where v is Element of E : (v + ((- 1) * B)) /\ ( the carrier of E \ A) <> {} } )

assume x in { v where v is Element of E : (v + ((- 1) * B)) /\ ( the carrier of E \ A) <> {} } ; :: thesis: ( x in the carrier of E & not x in { w where w is Element of E : w + ((- 1) * B) c= A } )
then consider v being Element of E such that
R2: ( x = v & (v + ((- 1) * B)) /\ ( the carrier of E \ A) <> {} ) ;
thus x in the carrier of E by R2; :: thesis: not x in { w where w is Element of E : w + ((- 1) * B) c= A }
thus not x in { w where w is Element of E : w + ((- 1) * B) c= A } :: thesis: verum

proof

assume x in { w where w is Element of E : w + ((- 1) * B) c= A } ; :: thesis: contradiction
then consider w being Element of E such that
R4: ( w = x & w + ((- 1) * B) c= A ) ;
v + ((- 1) * B) misses the carrier of E \ A by R2, R4, XBOOLE_1:85;
hence contradiction by R2, XBOOLE_0:def 7; :: thesis: verum

end;

end;

assume X5: ( x in the carrier of E & not x in { v where v is Element of E : v + ((- 1) * B) c= A } ) ; :: thesis: x in { v where v is Element of E : (v + ((- 1) * B)) /\ ( the carrier of E \ A) <> {} }
then reconsider w = x as Element of E ;

now :: thesis: not (w + ((- 1) * B)) /\ ( the carrier of E \ A) = {}

assume (w + ((- 1) * B)) /\ ( the carrier of E \ A) = {} ; :: thesis: contradiction
then {} = ((w + ((- 1) * B)) /\ the carrier of E) \ A by XBOOLE_1:49
.= (w + ((- 1) * B)) \ A by XBOOLE_1:28 ;
then w + ((- 1) * B) c= A by XBOOLE_1:37;
hence contradiction by X5; :: thesis: verum

end;

hence x in { v where v is Element of E : (v + ((- 1) * B)) /\ ( the carrier of E \ A) <> {} } ; :: thesis: verum

end;

X2: for x being set holds
( x in { v where v is Element of E : v + ((- 1) * B) c= the carrier of E \ A } iff ( x in the carrier of E & not x in { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} } ) )

proof

let x be set ; :: thesis: ( x in { v where v is Element of E : v + ((- 1) * B) c= the carrier of E \ A } iff ( x in the carrier of E & not x in { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} } ) )

hereby :: thesis: ( x in the carrier of E & not x in { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} } implies x in { v where v is Element of E : v + ((- 1) * B) c= the carrier of E \ A } )

assume x in { v where v is Element of E : v + ((- 1) * B) c= the carrier of E \ A } ; :: thesis: ( x in the carrier of E & not x in { w where w is Element of E : (w + ((- 1) * B)) /\ A <> {} } )
then consider v being Element of E such that
R2: ( x = v & v + ((- 1) * B) c= the carrier of E \ A ) ;
thus x in the carrier of E by R2; :: thesis: not x in { w where w is Element of E : (w + ((- 1) * B)) /\ A <> {} }
thus not x in { w where w is Element of E : (w + ((- 1) * B)) /\ A <> {} } :: thesis: verum

proof

assume x in { w where w is Element of E : (w + ((- 1) * B)) /\ A <> {} } ; :: thesis: contradiction
then consider w being Element of E such that
R4: ( w = x & (w + ((- 1) * B)) /\ A <> {} ) ;
w + ((- 1) * B) misses the carrier of E \ ( the carrier of E \ A) by R2, R4, XBOOLE_1:85;
then w + ((- 1) * B) misses the carrier of E /\ A by XBOOLE_1:48;
then w + ((- 1) * B) misses A by XBOOLE_1:28;
hence contradiction by R4, XBOOLE_0:def 7; :: thesis: verum

end;

end;

assume X5: ( x in the carrier of E & not x in { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} } ) ; :: thesis: x in { v where v is Element of E : v + ((- 1) * B) c= the carrier of E \ A }
then reconsider w = x as Element of E ;
reconsider w = x as Element of E by X5;
(w + ((- 1) * B)) \ ( the carrier of E \ A) = ((w + ((- 1) * B)) \ the carrier of E) \/ ((w + ((- 1) * B)) /\ A) by XBOOLE_1:52
.= {} \/ ((w + ((- 1) * B)) /\ A) by XBOOLE_1:37
.= {} by X5 ;
then w + ((- 1) * B) c= the carrier of E \ A by XBOOLE_1:37;
hence x in { v where v is Element of E : v + ((- 1) * B) c= the carrier of E \ A } ; :: thesis: verum

end;

thus ( the carrier of E \ A) (+) B = { v where v is Element of E : (v + ((- 1) * B)) /\ ( the carrier of E \ A) <> {} } by Th104, P1
.= the carrier of E \ { v where v is Element of E : v + ((- 1) * B) c= A } by X1, XBOOLE_0:def 5
.= the carrier of E \ (A (-) B) by Th105 ; :: thesis: ( the carrier of E \ A) (-) B = the carrier of E \ (A (+) B)
thus ( the carrier of E \ A) (-) B = { v where v is Element of E : v + ((- 1) * B) c= the carrier of E \ A } by Th105, P1
.= the carrier of E \ { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} } by X2, XBOOLE_0:def 5
.= the carrier of E \ (A (+) B) by Th104 ; :: thesis: verum

end;

end;