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

now :: thesis: for x being object st x in { (Sum l) where l is Linear_Combination of A : rng l c= RAT } holds
x in [#] X

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

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: verum