let Al be QC-alphabet ; :: thesis: for x, y being bound_QC-variable of Al
for s9 being QC-formula of Al st x <> y & not x in still_not-bound_in s9 holds
not x in still_not-bound_in (s9 . y)
let x, y be bound_QC-variable of Al; :: thesis: for s9 being QC-formula of Al 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 of Al; :: 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 Al] means ( x <> y & not x in still_not-bound_in $1 implies not x in still_not-bound_in ($1 . y) );

A1: now :: thesis: for s being Element of QC-WFF Al holds
( ( s is atomic implies S₁[s] ) & S₁[ VERUM Al] & ( 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] ) )

let s be Element of QC-WFF Al; :: thesis: ( ( s is atomic implies S₁[s] ) & S₁[ VERUM Al] & ( 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 Al] & ( 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),((Al a. 0) .--> y));
A5: still_not-bound_in s = still_not-bound_in (the_arguments_of s) by A2, QC_LANG3:4
.= variables_in ((the_arguments_of s),(bound_QC-variables Al)) by QC_LANG3:2
.= { ((the_arguments_of s) . k) where k is Nat : ( 1 <= k & k <= len (the_arguments_of s) & (the_arguments_of s) . k in bound_QC-variables Al ) } by QC_LANG3:def 1 ;
A6: ( x in { ((Subst ((the_arguments_of s),((Al a. 0) .--> y))) . k) where k is Nat : ( 1 <= k & k <= len (Subst ((the_arguments_of s),((Al a. 0) .--> y))) & (Subst ((the_arguments_of s),((Al a. 0) .--> y))) . k in bound_QC-variables Al ) } implies x in { ((the_arguments_of s) . i) where i is Nat : ( 1 <= i & i <= len (the_arguments_of s) & (the_arguments_of s) . i in bound_QC-variables Al ) } )

proof

assume x in { ((Subst ((the_arguments_of s),((Al a. 0) .--> y))) . k) where k is Nat : ( 1 <= k & k <= len (Subst ((the_arguments_of s),((Al a. 0) .--> y))) & (Subst ((the_arguments_of s),((Al a. 0) .--> y))) . k in bound_QC-variables Al ) } ; :: thesis: x in { ((the_arguments_of s) . i) where i is Nat : ( 1 <= i & i <= len (the_arguments_of s) & (the_arguments_of s) . i in bound_QC-variables Al ) }
then consider k being Nat such that
A7: x = (Subst ((the_arguments_of s),((Al a. 0) .--> y))) . k and
A8: 1 <= k and
A9: k <= len (Subst ((the_arguments_of s),((Al a. 0) .--> y))) and
(Subst ((the_arguments_of s),((Al a. 0) .--> y))) . k in bound_QC-variables Al ;
A10: k <= len (the_arguments_of s) by A9, CQC_LANG:def 1;
then x = (the_arguments_of s) . k by A3, A7, A8, CQC_LANG:3;
hence x in { ((the_arguments_of s) . i) where i is Nat : ( 1 <= i & i <= len (the_arguments_of s) & (the_arguments_of s) . i in bound_QC-variables Al ) } by A8, A10; :: thesis: verum

end;

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

proof

consider k being Nat, p being QC-pred_symbol of k,Al, l2 being QC-variable_list of k,Al such that
A13: s = p ! l2 by A2, QC_LANG1:def 18;
l2 = the_arguments_of s by A2, A13, QC_LANG1:def 23;
then reconsider l3 = Subst ((the_arguments_of s),((Al a. 0) .--> y)) as QC-variable_list of k,Al ;
A14: s . y = p ! l3 by A2, A11, A13, QC_LANG1:def 22;
hence s . y is atomic by QC_LANG1:def 18; :: thesis: the_arguments_of (s . y) = Subst ((the_arguments_of s),((Al a. 0) .--> y))
hence the_arguments_of (s . y) = Subst ((the_arguments_of s),((Al a. 0) .--> y)) by A14, QC_LANG1:def 23; :: thesis: verum

end;

then still_not-bound_in (the_arguments_of (s . y)) = variables_in ((Subst ((the_arguments_of s),((Al a. 0) .--> y))),(bound_QC-variables Al)) by QC_LANG3:2
.= { ((Subst ((the_arguments_of s),((Al a. 0) .--> y))) . k) where k is Nat : ( 1 <= k & k <= len (Subst ((the_arguments_of s),((Al a. 0) .--> y))) & (Subst ((the_arguments_of s),((Al a. 0) .--> y))) . k in bound_QC-variables Al ) } by QC_LANG3:def 1 ;
hence not x in still_not-bound_in (s . y) by A4, A5, A12, A6, QC_LANG3:4; :: thesis: verum

end;

end;

thus S₁[ VERUM Al] by CQC_LANG:15; :: 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:6, QC_LANG3:7;
hence not x in still_not-bound_in (s . y) by A15, CQC_LANG:18; :: 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:9;
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:10;
hence not x in still_not-bound_in (s . y) by A17, CQC_LANG:20; :: 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:11;
thus not x in still_not-bound_in (s . y) :: thesis: verum

proof

A24: now :: thesis: ( x in {(bound_in s)} implies not x in still_not-bound_in (s . y) )

still_not-bound_in (All (x,((the_scope_of s) . y))) = (still_not-bound_in ((the_scope_of s) . y)) \ {x} by QC_LANG3:12;
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:23, TARSKI:def 1; :: thesis: verum

end;

now :: thesis: ( not x in still_not-bound_in (the_scope_of s) implies not x in still_not-bound_in (s . y) )

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:12;
hence not x in still_not-bound_in (s . y) by A19, A22, CQC_LANG:22, CQC_LANG:23; :: 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 Al 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