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 and
A2: z1 in { (seq . k) where k is Element of NAT : n <= k } ;
ex k1 being Element of NAT st
( z1 = seq . k1 & n <= k1 ) by A2;
hence x in REAL by A1; :: thesis: verum

end;

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