let A be QC-alphabet ; :: thesis: for x being bound_QC-variable of A
for h being QC-formula of A holds still_not-bound_in h c= still_not-bound_in (h . x)
let x be bound_QC-variable of A; :: thesis: for h being QC-formula of A holds still_not-bound_in h c= still_not-bound_in (h . x)
defpred S1[ QC-formula of A] means still_not-bound_in $1 c= still_not-bound_in ($1 . x);
A1: for p being Element of QC-WFF A st S1[p] holds
S1[ 'not' p]
proof
let p be Element of QC-WFF A; :: thesis: ( S1[p] implies S1[ 'not' p] )
still_not-bound_in (('not' p) . x) = still_not-bound_in ('not' (p . x)) by CQC_LANG:19
.= still_not-bound_in (p . x) by QC_LANG3:7 ;
hence ( S1[p] implies S1[ 'not' p] ) by QC_LANG3:7; :: thesis: verum
end;
A2: for p, q being Element of QC-WFF A st S1[p] & S1[q] holds
S1[p '&' q]
proof
let p, q be Element of QC-WFF A; :: thesis: ( S1[p] & S1[q] implies S1[p '&' q] )
assume that
A3: S1[p] and
A4: S1[q] ; :: thesis: S1[p '&' q]
A5: still_not-bound_in ((p '&' q) . x) = still_not-bound_in ((p . x) '&' (q . x)) by CQC_LANG:21
.= (still_not-bound_in (p . x)) \/ (still_not-bound_in (q . x)) by QC_LANG3:10 ;
still_not-bound_in (p '&' q) = (still_not-bound_in p) \/ (still_not-bound_in q) by QC_LANG3:10;
hence S1[p '&' q] by A3, A4, A5, XBOOLE_1:13; :: thesis: verum
end;
A6: for x being bound_QC-variable of A
for p being Element of QC-WFF A st S1[p] holds
S1[ All (x,p)]
proof
let y be bound_QC-variable of A; :: thesis: for p being Element of QC-WFF A st S1[p] holds
S1[ All (y,p)]
let p be Element of QC-WFF A; :: thesis: ( S1[p] implies S1[ All (y,p)] )
assume A7: S1[p] ; :: thesis: S1[ All (y,p)]
per cases ( y = x or y <> x ) ;
suppose y = x ; :: thesis: S1[ All (y,p)]
hence S1[ All (y,p)] by CQC_LANG:24; :: thesis: verum
end;
end;
end;
A10: for k being Nat
for P being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds S1[P ! ll]
proof
let k be Nat; :: thesis: for P being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds S1[P ! ll]
let P be QC-pred_symbol of k,A; :: thesis: for ll being QC-variable_list of k,A holds S1[P ! ll]
let ll be QC-variable_list of k,A; :: thesis: S1[P ! ll]
A11: still_not-bound_in ((P ! ll) . x) = still_not-bound_in (P ! (Subst (ll,((A a. 0) .--> x)))) by CQC_LANG:17
.= still_not-bound_in (Subst (ll,((A a. 0) .--> x))) by QC_LANG3:5 ;
still_not-bound_in ll c= still_not-bound_in (Subst (ll,((A a. 0) .--> x))) by Th60;
hence S1[P ! ll] by A11, QC_LANG3:5; :: thesis: verum
end;
A12: S1[ VERUM A] by CQC_LANG:15;
thus for h being QC-formula of A holds S1[h] from QC_LANG1:sch 1(A10, A12, A1, A2, A6); :: thesis: verum