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_{1}( Nat) -> Element of ExtREAL = seq . $1;

defpred S_{1}[ Nat] means n <= $1;

set Y = { H_{1}(k) where k is Nat : S_{1}[k] } ;

A1: seq . n in { H_{1}(k) where k is Nat : S_{1}[k] }
;

{ H_{1}(k) where k is Nat : S_{1}[k] } c= ExtREAL

let n be Nat; :: thesis: { (seq . k) where k is Nat : n <= k } is non empty Subset of ExtREAL

deffunc H

defpred S

set Y = { H

A1: seq . n in { H

{ H

proof

hence
{ (seq . k) where k is Nat : n <= k } is non empty Subset of ExtREAL
by A1; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H_{1}(k) where k is Nat : S_{1}[k] } or x in ExtREAL )

assume x in { H_{1}(k) where k is Nat : S_{1}[k] }
; :: thesis: x in ExtREAL

then consider k being Nat such that

A2: H_{1}(k) = x
and

S_{1}[k]
;

thus x in ExtREAL by A2; :: thesis: verum

end;assume x in { H

then consider k being Nat such that

A2: H

S

thus x in ExtREAL by A2; :: thesis: verum