let A be QC-alphabet ; :: thesis: for p being QC-formula of A st p is conjunctive holds
still_not-bound_in p = (still_not-bound_in (the_left_argument_of p)) \/ (still_not-bound_in (the_right_argument_of p))
deffunc H₁( Element of QC-WFF A) -> Element of bool (bound_QC-variables A) = still_not-bound_in $1;
deffunc H₂( Element of QC-WFF A) -> Element of bool (bound_QC-variables A) = still_not-bound_in (the_arguments_of $1);
deffunc H₃( Element of QC-WFF A, Subset of (bound_QC-variables A)) -> Element of bool (bound_QC-variables A) = $2 \ {(bound_in $1)};
deffunc H₄( Subset of (bound_QC-variables A)) -> Subset of (bound_QC-variables A) = $1;
deffunc H₅( Subset of (bound_QC-variables A), Subset of (bound_QC-variables A)) -> Element of bool (bound_QC-variables A) = $1 \/ $2;
A1: for p being QC-formula of A
for d being Subset of (bound_QC-variables A) holds
( d = H₁(p) iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( d = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H₂(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H₄(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H₅(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H₃(p,d1) ) ) ) ) ) by Lm1;
let p be QC-formula of A; :: thesis: ( p is conjunctive implies still_not-bound_in p = (still_not-bound_in (the_left_argument_of p)) \/ (still_not-bound_in (the_right_argument_of p)) )
assume A2: p is conjunctive ; :: thesis: still_not-bound_in p = (still_not-bound_in (the_left_argument_of p)) \/ (still_not-bound_in (the_right_argument_of p))
for d1, d2 being Subset of (bound_QC-variables A) st d1 = H₁( the_left_argument_of p) & d2 = H₁( the_right_argument_of p) holds
H₁(p) = H₅(d1,d2) from QC_LANG3:sch 6(A1, A2);
hence still_not-bound_in p = (still_not-bound_in (the_left_argument_of p)) \/ (still_not-bound_in (the_right_argument_of p)) ; :: thesis: verum