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