let p, q be Element of CQC-WFF ; :: 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:14;
A2: NBI (p '&' q) c= NBI q

proof

let e be set ; :: 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 k being Element of NAT such that
A3: k = e and
A4: for i being Element of NAT st k <= i holds
not x. i in still_not-bound_in (p '&' q) ;

now

let i be Element of NAT ; :: thesis: ( k <= i implies not x. i in still_not-bound_in q )
assume A5: k <= i ; :: thesis: not x. i 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. i 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 set ; :: 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 k being Element of NAT such that
A6: k = e and
A7: for i being Element of NAT st k <= i holds
not x. i in still_not-bound_in (p '&' q) ;

now

let i be Element of NAT ; :: thesis: ( k <= i implies not x. i in still_not-bound_in p )
assume A8: k <= i ; :: thesis: not x. i 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. i 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, XXREAL_2:60; :: thesis: verum