defpred S₁[ Element of QC-WFF A] means Bound_Vars A is finite ;
A1: for p being Element of QC-WFF A holds
( ( p is atomic implies S₁[p] ) & S₁[ VERUM A] & ( 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 A; :: thesis:
thus ( p is atomic implies Bound_Vars p is finite ) :: thesis:

proof

deffunc H₁( set ) -> set = (the_arguments_of p) . A;
defpred S₂[ Nat] means ( 1 <= A & A <= len (the_arguments_of p) );
defpred S₃[ Nat] means ( 1 <= A & A <= len (the_arguments_of p) & (the_arguments_of p) . A in bound_QC-variables A );
A2: { H₁(k) where k is Nat : S₃[k] } c= { H₁(n) where n is Nat : S₂[n] }

proof

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in { H₁(k) where k is Nat : S₃[k] } ; :: thesis:
then ex k being Nat st
( e = H₁(k) & S₃[k] ) ;
hence e in { H₁(n) where n is Nat : S₂[n] } ; :: thesis:

end;

assume p is atomic ; :: thesis:
then Bound_Vars p = Bound_Vars (the_arguments_of p) by Lm1
.= { ((the_arguments_of p) . k) where k is Nat : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ;
then Bound_Vars p c= rng (the_arguments_of p) by A2, CQC_SIM1:9;
hence Bound_Vars p is finite ; :: thesis:

end;

thus Bound_Vars (VERUM A) is finite by Th2; :: thesis:
thus ( p is negative & Bound_Vars (the_argument_of p) is finite implies Bound_Vars p is finite ) by Lm1; :: thesis:
thus ( p is conjunctive & Bound_Vars (the_left_argument_of p) is finite & Bound_Vars (the_right_argument_of p) is finite implies Bound_Vars p is finite ) :: thesis:

proof

assume that
A3: p is conjunctive and
A4: ( Bound_Vars (the_left_argument_of p) is finite & Bound_Vars (the_right_argument_of p) is finite ) ; :: thesis:
Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) by A3, Lm1;
hence Bound_Vars p is finite by A4; :: thesis:

end;

assume that
A5: p is universal and
A6: Bound_Vars (the_scope_of p) is finite ; :: thesis:
Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} by A5, Lm1;
hence S₁[p] by A6; :: thesis:

end;

for p being Element of QC-WFF A holds S₁[p] from QC_LANG1:sch 2(A1);
hence Bound_Vars p is finite ; :: thesis: