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

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

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

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

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

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

then consider w being Element of E such that

A2: ( x = w & ( for c being Element of E st c in C holds

w - c in A ) ) ;

for c being Element of E st c in C holds

w - c in B by A1, A2;

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

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

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

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

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

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

then consider w being Element of E such that

A2: ( x = w & ( for c being Element of E st c in C holds

w - c in A ) ) ;

for c being Element of E st c in C holds

w - c in B by A1, A2;

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