let E be RealLinearSpace; :: thesis: for A, B, C being non empty binary-image of E st A c= B holds

C (-) B c= C (-) A

let A, B, C be non empty binary-image of E; :: thesis: ( A c= B implies C (-) B c= C (-) A )

assume A1: A c= B ; :: thesis: C (-) B c= C (-) A

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in C (-) B or x in C (-) A )

assume x in C (-) B ; :: thesis: x in C (-) A

then consider w being Element of E such that

A2: ( x = w & ( for b being Element of E st b in B holds

w - b in C ) ) ;

for a being Element of E st a in A holds

w - a in C by A1, A2;

hence x in C (-) A by A2; :: thesis: verum

C (-) B c= C (-) A

let A, B, C be non empty binary-image of E; :: thesis: ( A c= B implies C (-) B c= C (-) A )

assume A1: A c= B ; :: thesis: C (-) B c= C (-) A

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in C (-) B or x in C (-) A )

assume x in C (-) B ; :: thesis: x in C (-) A

then consider w being Element of E such that

A2: ( x = w & ( for b being Element of E st b in B holds

w - b in C ) ) ;

for a being Element of E st a in A holds

w - a in C by A1, A2;

hence x in C (-) A by A2; :: thesis: verum