let V be non empty RLSStruct ; :: thesis: for M, N being Subset of V
for x, y being VECTOR of V st x in M & y in N holds
x - y in M - N
let M, N be Subset of V; :: thesis: for x, y being VECTOR of V st x in M & y in N holds
x - y in M - N
let x, y be VECTOR of V; :: thesis: ( x in M & y in N implies x - y in M - N )
M - N = { (u - v) where u, v is VECTOR of V : ( u in M & v in N ) } by RUSUB_5:def 2;
hence ( x in M & y in N implies x - y in M - N ) ; :: thesis: verum