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