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 AS: A c= B ; :: thesis: A (-) C c= B (-) C
let x be set ; :: 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
P2: ( x = w & ( for c being Element of E st c in C holds
w - c in A ) ) ;

now :: thesis: for c being Element of E st c in C holds
w - c in B

let c be Element of E; :: thesis: ( c in C implies w - c in B )
assume c in C ; :: thesis: w - c in B
then w - c in A by P2;
hence w - c in B by AS; :: thesis: verum

end;

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