let A be QC-alphabet ; :: thesis:
let p, q be Element of CQC-WFF A; :: thesis:
A1: still_not-bound_in (p '&' q) = (still_not-bound_in p) \/ (still_not-bound_in q) by QC_LANG3:10;
A2: NBI (p '&' q) c= NBI q

proof

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in NBI (p '&' q) ; :: thesis:
then consider t being QC-symbol of A such that
A3: t = e and
A4: for u being QC-symbol of A st t <= u holds
not x. u in still_not-bound_in (p '&' q) ;

now :: thesis:

let u be QC-symbol of A; :: thesis:
assume A5: t <= u ; :: thesis:
still_not-bound_in q c= still_not-bound_in (p '&' q) by A1, XBOOLE_1:7;
hence not x. u in still_not-bound_in q by A4, A5; :: thesis:

end;

hence e in NBI q by A3; :: thesis:

end;

NBI (p '&' q) c= NBI p

proof

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in NBI (p '&' q) ; :: thesis:
then consider t being QC-symbol of A such that
A6: t = e and
A7: for u being QC-symbol of A st t <= u holds
not x. u in still_not-bound_in (p '&' q) ;

now :: thesis:

let u be QC-symbol of A; :: thesis:
assume A8: t <= u ; :: thesis:
still_not-bound_in p c= still_not-bound_in (p '&' q) by A1, XBOOLE_1:7;
hence not x. u in still_not-bound_in p by A7, A8; :: thesis:

end;

hence e in NBI p by A6; :: thesis:

end;

hence ( index p <= index (p '&' q) & index q <= index (p '&' q) ) by A2, QC_LANG1:28; :: thesis: