let Al be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF Al st still_not-bound_in p c= Bound_Vars p & still_not-bound_in q c= Bound_Vars q holds
still_not-bound_in (p '&' q) c= Bound_Vars (p '&' q)
let p, q be Element of CQC-WFF Al; :: thesis: ( still_not-bound_in p c= Bound_Vars p & still_not-bound_in q c= Bound_Vars q implies still_not-bound_in (p '&' q) c= Bound_Vars (p '&' q) )
A1: still_not-bound_in (p '&' q) = (still_not-bound_in p) \/ (still_not-bound_in q) by QC_LANG3:10;
p '&' q is conjunctive by QC_LANG1:def 20;
then Bound_Vars (p '&' q) = (Bound_Vars (the_left_argument_of (p '&' q))) \/ (Bound_Vars (the_right_argument_of (p '&' q))) by SUBSTUT1:5;
then Bound_Vars (p '&' q) = (Bound_Vars p) \/ (Bound_Vars (the_right_argument_of (p '&' q))) by QC_LANG2:4;
then A2: Bound_Vars (p '&' q) = (Bound_Vars p) \/ (Bound_Vars q) by QC_LANG2:4;
assume ( still_not-bound_in p c= Bound_Vars p & still_not-bound_in q c= Bound_Vars q ) ; :: thesis: still_not-bound_in (p '&' q) c= Bound_Vars (p '&' q)
hence still_not-bound_in (p '&' q) c= Bound_Vars (p '&' q) by A2, A1, XBOOLE_1:13; :: thesis: verum