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

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

hence
r * M c= r * N
; :: thesis: verum
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;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