let seq be Real_Sequence; :: thesis: for n being Element of NAT holds { (seq . k) where k is Element of NAT : n <= k } is Subset of REAL
let n be Element of NAT ; :: thesis: { (seq . k) where k is Element of NAT : n <= k } is Subset of REAL
set Y = { (seq . k) where k is Element of NAT : n <= k } ;

now

let x be set ; :: thesis: ( x in { (seq . k) where k is Element of NAT : n <= k } implies x in REAL )
assume x in { (seq . k) where k is Element of NAT : n <= k } ; :: thesis: x in REAL
then consider z1 being set such that
A1: ( z1 = x & z1 in { (seq . k) where k is Element of NAT : n <= k } ) ;
consider k1 being Element of NAT such that
A2: ( z1 = seq . k1 & n <= k1 ) by A1;
thus x in REAL by A1, A2; :: thesis: verum

end;

hence { (seq . k) where k is Element of NAT : n <= k } is Subset of REAL by TARSKI:def 3; :: thesis: verum