let r be Real; :: thesis: for RLS being non empty RLSStruct

for A, B being Subset of RLS st A c= B holds

r * A c= r * B

let RLS be non empty RLSStruct ; :: thesis: for A, B being Subset of RLS st A c= B holds

r * A c= r * B

let A, B be Subset of RLS; :: thesis: ( A c= B implies r * A c= r * B )

assume A1: A c= B ; :: thesis: r * A c= r * B

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in r * A or x in r * B )

assume x in r * A ; :: thesis: x in r * B

then ex v being Element of RLS st

( x = r * v & v in A ) ;

hence x in r * B by A1; :: thesis: verum

for A, B being Subset of RLS st A c= B holds

r * A c= r * B

let RLS be non empty RLSStruct ; :: thesis: for A, B being Subset of RLS st A c= B holds

r * A c= r * B

let A, B be Subset of RLS; :: thesis: ( A c= B implies r * A c= r * B )

assume A1: A c= B ; :: thesis: r * A c= r * B

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in r * A or x in r * B )

assume x in r * A ; :: thesis: x in r * B

then ex v being Element of RLS st

( x = r * v & v in A ) ;

hence x in r * B by A1; :: thesis: verum