defpred S₁[ Element of QC-WFF ] means still_not-bound_in $1 is finite ;
A1: for p being Element of QC-WFF holds
( ( p is atomic implies S₁[p] ) & S₁[ VERUM ] & ( p is negative & S₁[ the_argument_of p] implies S₁[p] ) & ( p is conjunctive & S₁[ the_left_argument_of p] & S₁[ the_right_argument_of p] implies S₁[p] ) & ( p is universal & S₁[ the_scope_of p] implies S₁[p] ) )

proof

let p be Element of QC-WFF ; :: thesis: ( ( p is atomic implies S₁[p] ) & S₁[ VERUM ] & ( p is negative & S₁[ the_argument_of p] implies S₁[p] ) & ( p is conjunctive & S₁[ the_left_argument_of p] & S₁[ the_right_argument_of p] implies S₁[p] ) & ( p is universal & S₁[ the_scope_of p] implies S₁[p] ) )
thus ( p is atomic implies still_not-bound_in p is finite ) :: thesis: ( S₁[ VERUM ] & ( p is negative & S₁[ the_argument_of p] implies S₁[p] ) & ( p is conjunctive & S₁[ the_left_argument_of p] & S₁[ the_right_argument_of p] implies S₁[p] ) & ( p is universal & S₁[ the_scope_of p] implies S₁[p] ) )

proof

assume p is atomic ; :: thesis: still_not-bound_in p is finite
then A2: still_not-bound_in p = still_not-bound_in (the_arguments_of p) by QC_LANG3:8
.= variables_in (the_arguments_of p),bound_QC-variables by QC_LANG3:6
.= { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables ) } ;
defpred S₂[ Element of NAT ] means ( 1 <= $1 & $1 <= len (the_arguments_of p) & (the_arguments_of p) . $1 in bound_QC-variables );
defpred S₃[ Element of NAT ] means ( 1 <= $1 & $1 <= len (the_arguments_of p) );
deffunc H₆( set ) -> set = (the_arguments_of p) . $1;
A3: for k being Element of NAT st S₂[k] holds
S₃[k] ;
{ H₆(k) where k is Element of NAT : S₂[k] } c= { H₆(n) where n is Element of NAT : S₃[n] } from FRAENKEL:sch 1(A3);
then ( still_not-bound_in p c= rng (the_arguments_of p) & rng (the_arguments_of p) is finite ) by A2, Th9;
hence still_not-bound_in p is finite ; :: thesis: verum

end;

thus still_not-bound_in VERUM is finite by QC_LANG3:7; :: thesis: ( ( p is negative & S₁[ the_argument_of p] implies S₁[p] ) & ( p is conjunctive & S₁[ the_left_argument_of p] & S₁[ the_right_argument_of p] implies S₁[p] ) & ( p is universal & S₁[ the_scope_of p] implies S₁[p] ) )
thus ( p is negative & still_not-bound_in (the_argument_of p) is finite implies still_not-bound_in p is finite ) by QC_LANG3:10; :: thesis: ( ( p is conjunctive & S₁[ the_left_argument_of p] & S₁[ the_right_argument_of p] implies S₁[p] ) & ( p is universal & S₁[ the_scope_of p] implies S₁[p] ) )
thus ( p is conjunctive & still_not-bound_in (the_left_argument_of p) is finite & still_not-bound_in (the_right_argument_of p) is finite implies still_not-bound_in p is finite ) :: thesis: ( p is universal & S₁[ the_scope_of p] implies S₁[p] )

proof

assume that
A4: p is conjunctive and
A5: ( still_not-bound_in (the_left_argument_of p) is finite & still_not-bound_in (the_right_argument_of p) is finite ) ; :: thesis: still_not-bound_in p is finite
still_not-bound_in p = (still_not-bound_in (the_left_argument_of p)) \/ (still_not-bound_in (the_right_argument_of p)) by A4, QC_LANG3:13;
hence still_not-bound_in p is finite by A5; :: thesis: verum

end;

assume that
A6: p is universal and
A7: still_not-bound_in (the_scope_of p) is finite ; :: thesis: S₁[p]
still_not-bound_in p = (still_not-bound_in (the_scope_of p)) \ {(bound_in p)} by A6, QC_LANG3:15;
hence S₁[p] by A7; :: thesis: verum

end;

thus for p being Element of QC-WFF holds S₁[p] from QC_LANG1:sch 2(A1); :: thesis: verum