let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A
for t being QC-symbol of A
for K being Element of Fin
for f being Element of Funcs (,) st [q,t,K,f] in SepQuadruples p holds
still_not-bound_in q c= \/ K

let p be Element of CQC-WFF A; :: thesis: for q being Element of CQC-WFF A
for t being QC-symbol of A
for K being Element of Fin
for f being Element of Funcs (,) st [q,t,K,f] in SepQuadruples p holds
still_not-bound_in q c= \/ K

deffunc H5( QC-formula of A) -> Element of bool = still_not-bound_in \$1;
defpred S1[ QC-formula of A, set , set , set ] means H5(\$1) c= H5(p) \/ \$3;
A1: for q being Element of CQC-WFF A
for t being QC-symbol of A
for K being Element of Fin
for f being Element of Funcs (,) st [(),t,K,f] in SepQuadruples p & S1[ 'not' q,t,K,f] holds
S1[q,t,K,f] by QC_LANG3:7;
A2: now :: thesis: for q, r being Element of CQC-WFF A
for t being QC-symbol of A
for K being Element of Fin
for f being Element of Funcs (,) st [(q '&' r),t,K,f] in SepQuadruples p & S1[q '&' r,t,K,f] holds
( S1[q,t,K,f] & S1[r,t + (),K,f] )
let q, r be Element of CQC-WFF A; :: thesis: for t being QC-symbol of A
for K being Element of Fin
for f being Element of Funcs (,) st [(q '&' r),t,K,f] in SepQuadruples p & S1[q '&' r,t,K,f] holds
( S1[q,t,K,f] & S1[r,t + (),K,f] )

let t be QC-symbol of A; :: thesis: for K being Element of Fin
for f being Element of Funcs (,) st [(q '&' r),t,K,f] in SepQuadruples p & S1[q '&' r,t,K,f] holds
( S1[q,t,K,f] & S1[r,t + (),K,f] )

let K be Element of Fin ; :: thesis: for f being Element of Funcs (,) st [(q '&' r),t,K,f] in SepQuadruples p & S1[q '&' r,t,K,f] holds
( S1[q,t,K,f] & S1[r,t + (),K,f] )

let f be Element of Funcs (,); :: thesis: ( [(q '&' r),t,K,f] in SepQuadruples p & S1[q '&' r,t,K,f] implies ( S1[q,t,K,f] & S1[r,t + (),K,f] ) )
assume that
[(q '&' r),t,K,f] in SepQuadruples p and
A3: S1[q '&' r,t,K,f] ; :: thesis: ( S1[q,t,K,f] & S1[r,t + (),K,f] )
A4: still_not-bound_in (q '&' r) = \/ by QC_LANG3:10;
then A5: still_not-bound_in r c= still_not-bound_in (q '&' r) by XBOOLE_1:7;
still_not-bound_in q c= still_not-bound_in (q '&' r) by ;
hence ( S1[q,t,K,f] & S1[r,t + (),K,f] ) by ; :: thesis: verum
end;
A6: now :: thesis: for q being Element of CQC-WFF A
for x being Element of bound_QC-variables A
for t being QC-symbol of A
for K being Element of Fin
for f being Element of Funcs (,) st [(All (x,q)),t,K,f] in SepQuadruples p & S1[ All (x,q),t,K,f] holds
S1[q,t ++ ,K \/ {x},f +* (x .--> (x. t))]
let q be Element of CQC-WFF A; :: thesis: for x being Element of bound_QC-variables A
for t being QC-symbol of A
for K being Element of Fin
for f being Element of Funcs (,) st [(All (x,q)),t,K,f] in SepQuadruples p & S1[ All (x,q),t,K,f] holds
S1[q,t ++ ,K \/ {x},f +* (x .--> (x. t))]

let x be Element of bound_QC-variables A; :: thesis: for t being QC-symbol of A
for K being Element of Fin
for f being Element of Funcs (,) st [(All (x,q)),t,K,f] in SepQuadruples p & S1[ All (x,q),t,K,f] holds
S1[q,t ++ ,K \/ {x},f +* (x .--> (x. t))]

let t be QC-symbol of A; :: thesis: for K being Element of Fin
for f being Element of Funcs (,) st [(All (x,q)),t,K,f] in SepQuadruples p & S1[ All (x,q),t,K,f] holds
S1[q,t ++ ,K \/ {x},f +* (x .--> (x. t))]

let K be Element of Fin ; :: thesis: for f being Element of Funcs (,) st [(All (x,q)),t,K,f] in SepQuadruples p & S1[ All (x,q),t,K,f] holds
S1[q,t ++ ,K \/ {x},f +* (x .--> (x. t))]

let f be Element of Funcs (,); :: thesis: ( [(All (x,q)),t,K,f] in SepQuadruples p & S1[ All (x,q),t,K,f] implies S1[q,t ++ ,K \/ {x},f +* (x .--> (x. t))] )
assume that
[(All (x,q)),t,K,f] in SepQuadruples p and
A7: S1[ All (x,q),t,K,f] ; :: thesis: S1[q,t ++ ,K \/ {x},f +* (x .--> (x. t))]
still_not-bound_in (All (x,q)) = \ {x} by QC_LANG3:12;
then still_not-bound_in q c= ( \/ K) \/ {x} by ;
hence S1[q,t ++ ,K \/ {x},f +* (x .--> (x. t))] by XBOOLE_1:4; :: thesis: verum
end;
A8: S1[p, index p, {}. , id ] ;
thus for q being Element of CQC-WFF A
for t being QC-symbol of A
for K being Element of Fin
for f being Element of Funcs (,) st [q,t,K,f] in SepQuadruples p holds
S1[q,t,K,f] from CQC_SIM1:sch 6(A8, A1, A2, A6); :: thesis: verum