set A = { k where k is Element of NAT : for i being Element of NAT st k <= i holds
not x. i in still_not-bound_in p } ;
ex k being Element of NAT st k in { k where k is Element of NAT : for i being Element of NAT st k <= i holds
not x. i in still_not-bound_in p }

proof

now

per cases ( still_not-bound_in p = {} or still_not-bound_in p <> {} ) ;

suppose still_not-bound_in p = {} ; :: thesis: ex k being Element of NAT st k in { k where k is Element of NAT : for i being Element of NAT st k <= i holds
not x. i in still_not-bound_in p }

then for i being Element of NAT st 0 <= i holds
not x. i in still_not-bound_in p ;
then 0 in { k where k is Element of NAT : for i being Element of NAT st k <= i holds
not x. i in still_not-bound_in p } ;
hence ex k being Element of NAT st k in { k where k is Element of NAT : for i being Element of NAT st k <= i holds
not x. i in still_not-bound_in p } ; :: thesis: verum

end;

suppose A1: still_not-bound_in p <> {} ; :: thesis: ex k being Element of NAT st k in { k where k is Element of NAT : for i being Element of NAT st k <= i holds
not x. i in still_not-bound_in p }

consider x being Element of still_not-bound_in p;
reconsider x = x as bound_QC-variable by A1, TARSKI:def 3;
consider i being Element of NAT such that
A2: x. i = x by QC_LANG3:36;
A3: ex a being set st a in { k where k is Element of NAT : x. k in still_not-bound_in p }

proof

take i ; :: thesis: i in { k where k is Element of NAT : x. k in still_not-bound_in p }
thus i in { k where k is Element of NAT : x. k in still_not-bound_in p } by A1, A2; :: thesis: verum

end;

A4: still_not-bound_in p is finite by Th20;
defpred S₁[ set , set ] means for n being Element of NAT st n = c₂ holds
x. n = p;
A5: for e being set st e in still_not-bound_in p holds
ex b being set st
( b in NAT & S₁[e,b] )

proof

let e be set ; :: thesis: ( e in still_not-bound_in p implies ex b being set st
( b in NAT & S₁[e,b] ) )
assume e in still_not-bound_in p ; :: thesis: ex b being set st
( b in NAT & S₁[e,b] )
then reconsider e = e as bound_QC-variable ;
consider i being Element of NAT such that
A6: x. i = e by QC_LANG3:36;
reconsider i = i as set ;
take i ; :: thesis: ( i in NAT & S₁[e,i] )
thus ( i in NAT & S₁[e,i] ) by A6; :: thesis: verum

end;

defpred S₂[ Element of NAT ] means x. p in still_not-bound_in p;
A7: { l where l is Element of NAT : S₂[l] } c= NAT from FRAENKEL:sch 10();
consider f being Function such that
A8: ( dom f = still_not-bound_in p & rng f c= NAT ) and
A9: for e being set st e in still_not-bound_in p holds
S₁[e,f . e] from WELLORD2:sch 1(A5);
reconsider f = f as Function of (still_not-bound_in p),NAT by A8, FUNCT_2:def 1, RELSET_1:11;

now

let y be set ; :: thesis: ( ( y in rng f implies y in { k where k is Element of NAT : x. k in still_not-bound_in p } ) & ( y in { k where k is Element of NAT : x. k in still_not-bound_in p } implies y in rng f ) )
thus ( y in rng f implies y in { k where k is Element of NAT : x. k in still_not-bound_in p } ) :: thesis: ( y in { k where k is Element of NAT : x. k in still_not-bound_in p } implies y in rng f )

proof

assume y in rng f ; :: thesis: y in { k where k is Element of NAT : x. k in still_not-bound_in p }
then consider x being set such that
A10: x in dom f and
A11: y = f . x by FUNCT_1:def 5;
reconsider n = f . x as Element of NAT ;
x. n in still_not-bound_in p by A8, A9, A10;
hence y in { k where k is Element of NAT : x. k in still_not-bound_in p } by A11; :: thesis: verum

end;

assume y in { k where k is Element of NAT : x. k in still_not-bound_in p } ; :: thesis: y in rng f
then consider k being Element of NAT such that
A12: ( y = k & x. k in still_not-bound_in p ) ;
reconsider a = x. k as Element of still_not-bound_in p by A12;
reconsider n = f . a as Element of NAT ;
x. n = x. k by A9, A12;
then n = k by ZFMISC_1:33;
hence y in rng f by A8, A12, FUNCT_1:def 5; :: thesis: verum

end;

then ( rng f = { k where k is Element of NAT : x. k in still_not-bound_in p } & dom f = still_not-bound_in p ) by FUNCT_2:def 1, TARSKI:2;
then A13: ( { k where k is Element of NAT : x. k in still_not-bound_in p } is finite & { n where n is Element of NAT : x. n in still_not-bound_in p } <> {} & { l where l is Element of NAT : x. l in still_not-bound_in p } c= NAT ) by A3, A4, A7;
defpred S₃[ Element of NAT , Element of NAT ] means c₂ <= p;
A14: for k, l being Element of NAT holds
( S₃[k,l] or S₃[l,k] ) ;
A15: for k, l, m being Element of NAT st S₃[k,l] & S₃[l,m] holds
S₃[k,m] by XXREAL_0:2;
consider m being Element of NAT such that
m in { k where k is Element of NAT : x. k in still_not-bound_in p } and
A16: for k being Element of NAT st k in { n where n is Element of NAT : x. n in still_not-bound_in p } holds
S₃[m,k] from CQC_SIM1:sch 4(A13, A14, A15);

now

take n = m + 1; :: thesis: ( n = m + 1 & ( for i being Element of NAT st m + 1 <= i holds
not x. i in still_not-bound_in p ) )
thus n = m + 1 ; :: thesis: for i being Element of NAT st m + 1 <= i holds
not x. i in still_not-bound_in p
let i be Element of NAT ; :: thesis: ( m + 1 <= i implies not x. i in still_not-bound_in p )
assume that
A17: m + 1 <= i and
A18: x. i in still_not-bound_in p ; :: thesis: contradiction
i in { l where l is Element of NAT : x. l in still_not-bound_in p } by A18;
then i <= m by A16;
hence contradiction by A17, NAT_1:13; :: thesis: verum

end;

then m + 1 in { k where k is Element of NAT : for i being Element of NAT st k <= i holds
not x. i in still_not-bound_in p } ;
hence ex k being Element of NAT st k in { k where k is Element of NAT : for i being Element of NAT st k <= i holds
not x. i in still_not-bound_in p } ; :: thesis: verum

end;

end;

end;

hence ex k being Element of NAT st k in { k where k is Element of NAT : for i being Element of NAT st k <= i holds
not x. i in still_not-bound_in p } ; :: thesis: verum

end;

hence not NBI p is empty ; :: thesis: verum