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 A1: ( A <> {} & B = {} ) ; :: thesis: B (-) A = B
then consider a being object such that
A2: a in A by XBOOLE_0:def 1;
reconsider a = a as Element of E by A2;
assume B (-) A <> B ; :: thesis: contradiction
then consider ba being object such that
A3: ba in B (-) A by A1, XBOOLE_0:def 1;
consider z being Element of E such that
A4: ( ba = z & ( for a being Element of E st a in A holds
z - a in B ) ) by A3;
thus contradiction by A1, A2, A4; :: thesis: verum