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

now :: thesis: for x being object st x in { (seq . k) where k is Nat : n <= k } holds
x in REAL

let x be object ; :: thesis: ( x in { (seq . k) where k is Nat : n <= k } implies x in REAL )
assume x in { (seq . k) where k is 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 Nat : n <= k } ;
consider k1 being Nat such that
A3: ( z1 = seq . k1 & n <= k1 ) by A2;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def 12;
z1 = seq . k1 by A3;
hence x in REAL by A1; :: thesis: verum

end;

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