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) )

( ( 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 )
;

end;

suppose A1:
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 A1, XBOOLE_1:37

.= {} by Th1

.= the carrier of E \ the carrier of E by XBOOLE_1:37

.= the carrier of E \ (A (-) B) by A1, Th4 ; :: thesis: ( the carrier of E \ A) (-) B = the carrier of E \ (A (+) B)

thus ( the carrier of E \ A) (-) B = X (-) B by A1, XBOOLE_1:37

.= {} by Th2

.= the carrier of E \ the carrier of E by XBOOLE_1:37

.= the carrier of E \ (A (+) B) by A1, Th3 ; :: thesis: verum

end;thus ( the carrier of E \ A) (+) B = X (+) B by A1, XBOOLE_1:37

.= {} by Th1

.= the carrier of E \ the carrier of E by XBOOLE_1:37

.= the carrier of E \ (A (-) B) by A1, Th4 ; :: thesis: ( the carrier of E \ A) (-) B = the carrier of E \ (A (+) B)

thus ( the carrier of E \ A) (-) B = X (-) B by A1, XBOOLE_1:37

.= {} by Th2

.= the carrier of E \ the carrier of E by XBOOLE_1:37

.= the carrier of E \ (A (+) B) by A1, Th3 ; :: thesis: verum

suppose A2:
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) )

A3:
not the carrier of E \ A is empty
by XBOOLE_1:37, A2;

A4: for x being object 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 } ) )

( 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 <> {} } ) )

.= the carrier of E \ { v where v is Element of E : v + ((- 1) * B) c= A } by A4, XBOOLE_0:def 5

.= the carrier of E \ (A (-) B) by Th8 ; :: 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 Th8, A3

.= the carrier of E \ { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} } by A8, XBOOLE_0:def 5

.= the carrier of E \ (A (+) B) by Th7 ; :: thesis: verum

end;A4: for x being object 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

A8:
for x being object holds
let x be object ; :: 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 } ) )

then reconsider w = x as Element of E ;

end;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 A7:
( 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) <> {} } 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

A5: ( x = v & (v + ((- 1) * B)) /\ ( the carrier of E \ A) <> {} ) ;

thus x in the carrier of E by A5; :: 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

end;then consider v being Element of E such that

A5: ( x = v & (v + ((- 1) * B)) /\ ( the carrier of E \ A) <> {} ) ;

thus x in the carrier of E by A5; :: 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

then reconsider w = x as Element of E ;

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

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

end;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 A7; :: thesis: verum

( 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

thus ( the carrier of E \ A) (+) B =
{ v where v is Element of E : (v + ((- 1) * B)) /\ ( the carrier of E \ A) <> {} }
by Th7, A3
let x be object ; :: 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 <> {} } ) )

then reconsider w = x as Element of E ;

reconsider w = x as Element of E by A11;

(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 A11 ;

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;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 A11:
( 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 } 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

A9: ( x = v & v + ((- 1) * B) c= the carrier of E \ A ) ;

thus x in the carrier of E by A9; :: 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

end;then consider v being Element of E such that

A9: ( x = v & v + ((- 1) * B) c= the carrier of E \ A ) ;

thus x in the carrier of E by A9; :: 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

A10: ( w = x & (w + ((- 1) * B)) /\ A <> {} ) ;

w + ((- 1) * B) misses the carrier of E \ ( the carrier of E \ A) by A9, A10, 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 A10; :: thesis: verum

end;then consider w being Element of E such that

A10: ( w = x & (w + ((- 1) * B)) /\ A <> {} ) ;

w + ((- 1) * B) misses the carrier of E \ ( the carrier of E \ A) by A9, A10, 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 A10; :: thesis: verum

then reconsider w = x as Element of E ;

reconsider w = x as Element of E by A11;

(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 A11 ;

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

.= the carrier of E \ { v where v is Element of E : v + ((- 1) * B) c= A } by A4, XBOOLE_0:def 5

.= the carrier of E \ (A (-) B) by Th8 ; :: 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 Th8, A3

.= the carrier of E \ { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} } by A8, XBOOLE_0:def 5

.= the carrier of E \ (A (+) B) by Th7 ; :: thesis: verum