defpred S1[ Nat] means r in F . $1; A8:
ex k being Nat st S1[k]
byA5, A7;
ex k being Nat st ( S1[k] & ( for n being Nat st S1[n] holds k <= n ) )
fromNAT_1:sch 5(A8); then consider k being Nat such that A9:
r in F . k
and A10:
for n being Nat st r in F . n holds k <= n
; A11:
( ex l being Nat st k = l + 1 implies ex s1 being Element of NAT st r in H . s1 )