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

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