let E be RealLinearSpace; :: thesis: for A, B being Subset of E st A <> {} & B = {} holds
B (-) A = B
let A, B be Subset of E; :: thesis: ( A <> {} & B = {} implies B (-) A = B )
assume AS: ( A <> {} & B = {} ) ; :: thesis: B (-) A = B
then consider a being set such that
P1: a in A by XBOOLE_0:def 1;
reconsider a = a as Element of E by P1;
assume B (-) A <> B ; :: thesis: contradiction
then consider ba being set such that
P2: ba in B (-) A by AS, XBOOLE_0:def 1;
consider z being Element of E such that
P3: ( ba = z & ( for a being Element of E st a in A holds
z - a in B ) ) by P2;
thus contradiction by AS, P1, P3; :: thesis: verum