let p be Element of CQC-WFF ; :: thesis: still_not-bound_in {p} = still_not-bound_in p

A1: now

let a be set ; :: 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 : q in {p} } ) by TARSKI:def 4;
ex q being Element of CQC-WFF 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

let a be set ; :: 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 : 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:1; :: thesis: verum