let x, y be bound_QC-variable; :: thesis: for s9 being QC-formula st x <> y & not x in still_not-bound_in s9 holds
not x in still_not-bound_in (s9 . y)
let s9 be QC-formula; :: thesis: ( x <> y & not x in still_not-bound_in s9 implies not x in still_not-bound_in (s9 . y) )
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: ( ( s is atomic implies S₁[s] ) & S₁[ VERUM ] & ( s is negative & S₁[ the_argument_of s] implies S₁[s] ) & ( s is conjunctive & S₁[ the_left_argument_of s] & S₁[ the_right_argument_of s] implies S₁[s] ) & ( s is universal & S₁[ the_scope_of s] implies S₁[s] ) )
thus ( s is atomic implies S₁[s] ) :: thesis: ( S₁[ VERUM ] & ( s is negative & S₁[ the_argument_of s] implies S₁[s] ) & ( s is conjunctive & S₁[ the_left_argument_of s] & S₁[ the_right_argument_of s] implies S₁[s] ) & ( s is universal & S₁[ the_scope_of s] implies S₁[s] ) )

proof

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

proof

set l = the_arguments_of s;
set ll = Subst ((the_arguments_of s),((a. 0) .--> y));
A5: still_not-bound_in s = still_not-bound_in (the_arguments_of s) by A2, QC_LANG3:8
.= variables_in ((the_arguments_of s),bound_QC-variables) by QC_LANG3:6
.= { ((the_arguments_of s) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of s) & (the_arguments_of s) . k in bound_QC-variables ) } by QC_LANG3:def 2 ;
A6: ( 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 ) } implies 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 ) } )

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: 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 ) }
then consider k being Element of NAT such that
A7: x = (Subst ((the_arguments_of s),((a. 0) .--> y))) . k and
A8: 1 <= k and
A9: k <= len (Subst ((the_arguments_of s),((a. 0) .--> y))) and
(Subst ((the_arguments_of s),((a. 0) .--> y))) . k in bound_QC-variables ;
A10: k <= len (the_arguments_of s) by A9, CQC_LANG:def 3;
then x = (the_arguments_of s) . k by A3, A7, A8, 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 A8, A10; :: thesis: verum

end;

A11: s . y = (the_pred_symbol_of s) ! (Subst ((the_arguments_of s),((a. 0) .--> y))) by A2, CQC_LANG:29;
A12: ( s . y is atomic & the_arguments_of (s . y) = Subst ((the_arguments_of s),((a. 0) .--> y)) )

proof

consider k being Element of NAT , p being QC-pred_symbol of k, l2 being QC-variable_list of k such that
A13: s = p ! l2 by A2, QC_LANG1:def 17;
l2 = the_arguments_of s by A2, A13, 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 k by FINSEQ_1:def 18;
A14: s . y = p ! l3 by A2, A11, A13, QC_LANG1:def 21;
hence s . y is atomic by QC_LANG1:def 17; :: thesis: the_arguments_of (s . y) = Subst ((the_arguments_of s),((a. 0) .--> y))
hence the_arguments_of (s . y) = Subst ((the_arguments_of s),((a. 0) .--> y)) by A14, QC_LANG1:def 22; :: thesis: verum

end;

then still_not-bound_in (the_arguments_of (s . y)) = variables_in ((Subst ((the_arguments_of s),((a. 0) .--> y))),bound_QC-variables) by QC_LANG3:6
.= { ((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 ) } by QC_LANG3:def 2 ;
hence not x in still_not-bound_in (s . y) by A4, A5, A12, A6, QC_LANG3:8; :: thesis: verum

end;

end;

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

proof

assume that
A15: s is negative and
A16: ( ( 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) ) & x <> y & not x in still_not-bound_in s ) ; :: thesis: not x in still_not-bound_in (s . y)
not x in still_not-bound_in ('not' ((the_argument_of s) . y)) by A15, A16, QC_LANG3:10, QC_LANG3:11;
hence not x in still_not-bound_in (s . y) by A15, CQC_LANG:31; :: thesis: verum

end;

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

proof

assume that
A17: s is conjunctive and
A18: ( ( x <> y & not x in still_not-bound_in (the_left_argument_of s) implies not x in still_not-bound_in ((the_left_argument_of s) . y) ) & ( x <> y & not x in still_not-bound_in (the_right_argument_of s) implies not x in still_not-bound_in ((the_right_argument_of s) . y) ) & x <> y & not x in still_not-bound_in s ) ; :: thesis: not x in still_not-bound_in (s . y)
still_not-bound_in s = (still_not-bound_in (the_left_argument_of s)) \/ (still_not-bound_in (the_right_argument_of s)) by A17, QC_LANG3:13;
then not x in (still_not-bound_in ((the_left_argument_of s) . y)) \/ (still_not-bound_in ((the_right_argument_of s) . y)) by A18, XBOOLE_0:def 3;
then not x in still_not-bound_in (((the_left_argument_of s) . y) '&' ((the_right_argument_of s) . y)) by QC_LANG3:14;
hence not x in still_not-bound_in (s . y) by A17, CQC_LANG:33; :: thesis: verum

end;

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

proof

assume that
A19: s is universal and
A20: ( x <> y & not x in still_not-bound_in (the_scope_of s) implies not x in still_not-bound_in ((the_scope_of s) . y) ) and
A21: x <> y and
A22: not x in still_not-bound_in s ; :: thesis: not x in still_not-bound_in (s . y)
A23: still_not-bound_in s = (still_not-bound_in (the_scope_of s)) \ {(bound_in s)} by A19, QC_LANG3:15;
thus not x in still_not-bound_in (s . y) :: thesis: verum

proof

A24: now

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 A25: ( ( 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;
assume x in {(bound_in s)} ; :: thesis: not x in still_not-bound_in (s . y)
then x = bound_in s by TARSKI:def 1;
hence not x in still_not-bound_in (s . y) by A19, A21, A25, CQC_LANG:36, TARSKI:def 1; :: thesis: verum

end;

now

assume not x in still_not-bound_in (the_scope_of s) ; :: thesis: not x in still_not-bound_in (s . y)
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, A22, CQC_LANG:35, CQC_LANG:36; :: thesis: verum

end;

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

end;

end;

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 s9 implies not x in still_not-bound_in (s9 . y) ) ; :: thesis: verum