let x, y be bound_QC-variable; :: thesis:
let s' be QC-formula; :: thesis:
defpred S₁[ Element of QC-WFF ] means ( x <> y & not x in still_not-bound_in $1 implies not x in still_not-bound_in ($1 . y) );

A1: now

let s be Element of QC-WFF ; :: thesis:
thus ( s is atomic implies S₁[s] ) :: thesis:

assume that
A2: s is atomic and
A3: ( x <> y & not x in still_not-bound_in s ) ; :: thesis:
thus not x in still_not-bound_in (s . y) :: thesis:

consider k being Element of NAT , p being QC-pred_symbol of k, l2 being QC-variable_list of such that
A7: s = p ! l2 by A2, QC_LANG1:def 17;
l2 = the_arguments_of s by A2, A7, QC_LANG1:def 22;
then len (the_arguments_of s) = k by FINSEQ_1:def 18;
then len (Subst (the_arguments_of s),((a. 0 ) .--> y)) = k by CQC_LANG:def 3;
then reconsider l3 = Subst (the_arguments_of s),((a. 0 ) .--> y) as QC-variable_list of by FINSEQ_1:def 18;
A8: s . y = p ! l3 by A2, A5, A7, QC_LANG1:def 21;
hence s . y is atomic by QC_LANG1:def 17; :: thesis:
hence the_arguments_of (s . y) = Subst (the_arguments_of s),((a. 0 ) .--> y) by A8, QC_LANG1:def 22; :: thesis:

end;

proof

assume x in { ((Subst (the_arguments_of s),((a. 0 ) .--> y)) . k) where k is Element of NAT : ( 1 <= k & k <= len (Subst (the_arguments_of s),((a. 0 ) .--> y)) & (Subst (the_arguments_of s),((a. 0 ) .--> y)) . k in bound_QC-variables ) } ; :: thesis:
then consider k being Element of NAT such that
A10: ( x = (Subst (the_arguments_of s),((a. 0 ) .--> y)) . k & 1 <= k & k <= len (Subst (the_arguments_of s),((a. 0 ) .--> y)) & (Subst (the_arguments_of s),((a. 0 ) .--> y)) . k in bound_QC-variables ) ;
A11: ( 1 <= k & k <= len (the_arguments_of s) ) by A10, CQC_LANG:def 3;
then ( x = (the_arguments_of s) . k & (the_arguments_of s) . k in bound_QC-variables ) by A3, A10, CQC_LANG:11;
hence x in { ((the_arguments_of s) . i) where i is Element of NAT : ( 1 <= i & i <= len (the_arguments_of s) & (the_arguments_of s) . i in bound_QC-variables ) } by A11; :: thesis:

end;

hence not x in still_not-bound_in (s . y) by A3, A4, A6, A9, QC_LANG3:8; :: thesis:

end;

thus S₁[ VERUM ] by CQC_LANG:28; :: thesis:
thus ( s is negative & S₁[ the_argument_of s] implies S₁[s] ) :: thesis:

assume that
A12: s is negative and
A13: ( x <> y & not x in still_not-bound_in (the_argument_of s) implies not x in still_not-bound_in ((the_argument_of s) . y) ) and
A14: ( x <> y & not x in still_not-bound_in s ) ; :: thesis:
not x in still_not-bound_in ('not' ((the_argument_of s) . y)) by A12, A13, A14, QC_LANG3:10, QC_LANG3:11;
hence not x in still_not-bound_in (s . y) by A12, CQC_LANG:31; :: thesis:

end;

thus ( s is conjunctive & S₁[ the_left_argument_of s] & S₁[ the_right_argument_of s] implies S₁[s] ) :: thesis:

end;

thus ( s is universal & S₁[ the_scope_of s] implies S₁[s] ) :: thesis:

A23: now

assume not x in still_not-bound_in (the_scope_of s) ; :: thesis:
then not x in (still_not-bound_in ((the_scope_of s) . y)) \ {(bound_in s)} by A20, A21, XBOOLE_0:def 5;
then not x in still_not-bound_in (All (bound_in s),((the_scope_of s) . y)) by QC_LANG3:16;
hence not x in still_not-bound_in (s . y) by A19, A21, CQC_LANG:35, CQC_LANG:36; :: thesis:

end;

now

assume x in {(bound_in s)} ; :: thesis:
then A24: x = bound_in s by TARSKI:def 1;
still_not-bound_in (All x,((the_scope_of s) . y)) = (still_not-bound_in ((the_scope_of s) . y)) \ {x} by QC_LANG3:16;
then ( ( not x in still_not-bound_in ((the_scope_of s) . y) or x in {x} ) iff not x in still_not-bound_in (All x,((the_scope_of s) . y)) ) by XBOOLE_0:def 5;
hence not x in still_not-bound_in (s . y) by A19, A21, A24, CQC_LANG:36, TARSKI:def 1; :: thesis:

end;

hence not x in still_not-bound_in (s . y) by A21, A22, A23, XBOOLE_0:def 5; :: thesis:

end;

for s being Element of QC-WFF holds S₁[s] from QC_LANG1:sch 2(A1);
hence ( x <> y & not x in still_not-bound_in s' implies not x in still_not-bound_in (s' . y) ) ; :: thesis: