defpred S1[ Nat] means r in F . $1; A21:
ex k being Nat st S1[k]
byA18, A20;
ex k being Nat st ( S1[k] & ( for n being Nat st S1[n] holds k <= n ) )
fromNAT_1:sch 5(A21); then consider k being Nat such that A22:
r in F . k
and A23:
for n being Nat st r in F . n holds k <= n
; A24:
( ex l being Nat st k = l + 1 implies ex s1 being Element of NAT st r in H . s1 )