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 H1( Nat) -> Element of ExtREAL = seq . $1;
defpred S1[ Nat] means n <= $1;
set Y = { H1(k) where k is Nat : S1[k] } ;
A1: seq . n in { H1(k) where k is Nat : S1[k] } ;
{ H1(k) where k is Nat : S1[k] } c= ExtREAL
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H1(k) where k is Nat : S1[k] } or x in ExtREAL )
assume x in { H1(k) where k is Nat : S1[k] } ; :: thesis: x in ExtREAL
then consider k being Nat such that
A2: H1(k) = x and
S1[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