let x be bound_QC-variable; :: thesis: for h being QC-formula holds still_not-bound_in h c= still_not-bound_in (h . x)
defpred S₁[ QC-formula] means still_not-bound_in $1 c= still_not-bound_in ($1 . x);
A1: for k being Element of NAT
for P being QC-pred_symbol of k
for ll being QC-variable_list of holds S₁[P ! ll]

proof

let k be Element of NAT ; :: thesis: for P being QC-pred_symbol of k
for ll being QC-variable_list of holds S₁[P ! ll]
let P be QC-pred_symbol of k; :: thesis: for ll being QC-variable_list of holds S₁[P ! ll]
let ll be QC-variable_list of ; :: thesis: S₁[P ! ll]
A2: still_not-bound_in ll c= still_not-bound_in (Subst ll,((a. 0 ) .--> x)) by Th61;
still_not-bound_in ((P ! ll) . x) = still_not-bound_in (P ! (Subst ll,((a. 0 ) .--> x))) by CQC_LANG:30
.= still_not-bound_in (Subst ll,((a. 0 ) .--> x)) by QC_LANG3:9 ;
hence S₁[P ! ll] by A2, QC_LANG3:9; :: thesis: verum

end;

A3: S₁[ VERUM ] by CQC_LANG:28;
A4: for p being Element of QC-WFF st S₁[p] holds
S₁[ 'not' p]

proof

let p be Element of QC-WFF ; :: thesis: ( S₁[p] implies S₁[ 'not' p] )
still_not-bound_in (('not' p) . x) = still_not-bound_in ('not' (p . x)) by CQC_LANG:32
.= still_not-bound_in (p . x) by QC_LANG3:11 ;
hence ( S₁[p] implies S₁[ 'not' p] ) by QC_LANG3:11; :: thesis: verum

end;

A5: for p, q being Element of QC-WFF st S₁[p] & S₁[q] holds
S₁[p '&' q]

proof

let p, q be Element of QC-WFF ; :: thesis: ( S₁[p] & S₁[q] implies S₁[p '&' q] )
assume that
A6: S₁[p] and
A7: S₁[q] ; :: thesis: S₁[p '&' q]
A8: still_not-bound_in (p '&' q) = (still_not-bound_in p) \/ (still_not-bound_in q) by QC_LANG3:14;
still_not-bound_in ((p '&' q) . x) = still_not-bound_in ((p . x) '&' (q . x)) by CQC_LANG:34
.= (still_not-bound_in (p . x)) \/ (still_not-bound_in (q . x)) by QC_LANG3:14 ;
hence S₁[p '&' q] by A6, A7, A8, XBOOLE_1:13; :: thesis: verum

end;

A9: for x being bound_QC-variable
for p being Element of QC-WFF st S₁[p] holds
S₁[ All x,p]

proof

let y be bound_QC-variable; :: thesis: for p being Element of QC-WFF st S₁[p] holds
S₁[ All y,p]
let p be Element of QC-WFF ; :: thesis: ( S₁[p] implies S₁[ All y,p] )
assume A10: S₁[p] ; :: thesis: S₁[ All y,p]

per cases ( y = x or y <> x ) ;

suppose y = x ; :: thesis: S₁[ All y,p]

hence S₁[ All y,p] by CQC_LANG:37; :: thesis: verum

end;

suppose y <> x ; :: thesis: S₁[ All y,p]

then A11: still_not-bound_in ((All y,p) . x) = still_not-bound_in (All y,(p . x)) by CQC_LANG:38
.= (still_not-bound_in (p . x)) \ {y} by QC_LANG3:16 ;
still_not-bound_in (All y,p) = (still_not-bound_in p) \ {y} by QC_LANG3:16;
hence S₁[ All y,p] by A10, A11, XBOOLE_1:33; :: thesis: verum

end;

end;

end;

thus for h being QC-formula holds S₁[h] from QC_LANG1:sch 1(A1, A3, A4, A5, A9); :: thesis: verum