let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al holds still_not-bound_in {p} = still_not-bound_in p
let p be Element of CQC-WFF Al; :: thesis: still_not-bound_in {p} = still_not-bound_in p

A1: now :: thesis: for a being object st a in still_not-bound_in {p} holds
a in still_not-bound_in p

let a be object ; :: thesis: ( a in still_not-bound_in {p} implies a in still_not-bound_in p )
assume a in still_not-bound_in {p} ; :: thesis: a in still_not-bound_in p
then consider b being set such that
A2: ( a in b & b in { (still_not-bound_in q) where q is Element of CQC-WFF Al : q in {p} } ) by TARSKI:def 4;
ex q being Element of CQC-WFF Al st
( b = still_not-bound_in q & q in {p} ) by A2;
hence a in still_not-bound_in p by A2, TARSKI:def 1; :: thesis: verum

end;

now :: thesis: for a being object st a in still_not-bound_in p holds
a in still_not-bound_in {p}

let a be object ; :: thesis: ( a in still_not-bound_in p implies a in still_not-bound_in {p} )
assume A3: a in still_not-bound_in p ; :: thesis: a in still_not-bound_in {p}
set b = still_not-bound_in p;
p in {p} by TARSKI:def 1;
then still_not-bound_in p in { (still_not-bound_in q) where q is Element of CQC-WFF Al : q in {p} } ;
hence a in still_not-bound_in {p} by A3, TARSKI:def 4; :: thesis: verum

end;

hence still_not-bound_in {p} = still_not-bound_in p by A1, TARSKI:2; :: thesis: verum