set S = { (Sum l) where l is Linear_Combination of A : rng l c= RAT } ;

now :: thesis:

let x be object ; :: thesis:
assume x in { (Sum l) where l is Linear_Combination of A : rng l c= RAT } ; :: thesis:
then ex l being Linear_Combination of A st
( x = Sum l & rng l c= RAT ) ;
hence x in [#] X ; :: thesis:

end;

then { (Sum l) where l is Linear_Combination of A : rng l c= RAT } c= [#] X ;
hence { (Sum l) where l is Linear_Combination of A : rng l c= RAT } is Subset of X ; :: thesis: