let V be non empty RLSStruct ; :: thesis: for M, N being Subset of V
for r being Real st M c= N holds
r * M c= r * N
let M, N be Subset of V; :: thesis: for r being Real st M c= N holds
r * M c= r * N
let r be Real; :: thesis: ( M c= N implies r * M c= r * N )
assume A1: M c= N ; :: thesis: r * M c= r * N
for x being VECTOR of V st x in r * M holds
x in r * N
proof
let x be VECTOR of V; :: thesis: ( x in r * M implies x in r * N )
assume x in r * M ; :: thesis: x in r * N
then ex w being VECTOR of V st
( x = r * w & w in M ) ;
hence x in r * N by A1; :: thesis: verum
end;
hence r * M c= r * N ; :: thesis: verum