defpred S₁[ Element of QC-WFF ] means Bound_Vars p 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 Bound_Vars 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

deffunc H₁( set ) -> set = (the_arguments_of p) . p;
defpred S₂[ Element of NAT ] means ( 1 <= p & p <= len (the_arguments_of p) );
defpred S₃[ Element of NAT ] means ( 1 <= p & p <= len (the_arguments_of p) & (the_arguments_of p) . p in bound_QC-variables );
A2: for k being Element of NAT st S₃[k] holds
S₂[k] ;
A3: { 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(A2);
assume p is atomic ; :: thesis: Bound_Vars p is finite
then Bound_Vars p = Bound_Vars (the_arguments_of p) by Lm1
.= { ((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 ) } ;
then Bound_Vars p c= rng (the_arguments_of p) by A3, CQC_SIM1:9;
hence Bound_Vars p is finite ; :: thesis: verum

end;

thus Bound_Vars VERUM is finite by Lm1; :: 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 & Bound_Vars (the_argument_of p) is finite implies Bound_Vars p is finite ) by Lm1; :: 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 & 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: ( p is universal & S₁[ the_scope_of p] implies S₁[p] )

proof

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

end;

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

end;

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