let seq be ExtREAL_sequence; :: thesis: for n being Nat holds { (seq . k) where k is Nat : n <= k } is non empty Subset of ExtREAL
let n be Nat; :: thesis: { (seq . k) where k is Nat : n <= k } is non empty Subset of ExtREAL
deffunc H₁( Nat) -> Element of ExtREAL = seq . $1;
defpred S₁[ Nat] means n <= $1;
set Y = { H₁(k) where k is Nat : S₁[k] } ;
A1: seq . n in { H₁(k) where k is Nat : S₁[k] } ;
{ H₁(k) where k is Nat : S₁[k] } c= ExtREAL

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H₁(k) where k is Nat : S₁[k] } or x in ExtREAL )
assume x in { H₁(k) where k is Nat : S₁[k] } ; :: thesis: x in ExtREAL
then consider k being Nat such that
A2: H₁(k) = x and
S₁[k] ;
thus x in ExtREAL by A2; :: thesis: verum

end;

hence { (seq . k) where k is Nat : n <= k } is non empty Subset of ExtREAL by A1; :: thesis: verum