let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A holds
( index p <= index (p '&' q) & index q <= index (p '&' q) )
let p, q be Element of CQC-WFF A; :: thesis: ( index p <= index (p '&' q) & index q <= index (p '&' q) )
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: ( not e in NBI (p '&' q) or e in NBI q )
assume e in NBI (p '&' q) ; :: thesis: e in NBI q
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: for u being QC-symbol of A st t <= u holds
not x. u in still_not-bound_in q

let u be QC-symbol of A; :: thesis: ( t <= u implies not x. u in still_not-bound_in q )
assume A5: t <= u ; :: thesis: not x. u in still_not-bound_in q
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: verum

end;

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

end;

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

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in NBI (p '&' q) or e in NBI p )
assume e in NBI (p '&' q) ; :: thesis: e in NBI p
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: for u being QC-symbol of A st t <= u holds
not x. u in still_not-bound_in p

let u be QC-symbol of A; :: thesis: ( t <= u implies not x. u in still_not-bound_in p )
assume A8: t <= u ; :: thesis: not x. u in still_not-bound_in p
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: verum

end;

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

end;

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