let Al be QC-alphabet ; :: thesis: for X, Y being Subset of (CQC-WFF Al) st X c= Y holds
still_not-bound_in X c= still_not-bound_in Y
let X, Y be Subset of (CQC-WFF Al); :: thesis: ( X c= Y implies still_not-bound_in X c= still_not-bound_in Y )
set A = { (still_not-bound_in p) where p is Element of CQC-WFF Al : p in X } ;
assume A1: X c= Y ; :: thesis: still_not-bound_in X c= still_not-bound_in Y
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in still_not-bound_in X or a in still_not-bound_in Y )
assume a in still_not-bound_in X ; :: thesis: a in still_not-bound_in Y
then consider b being set such that
A2: a in b and
A3: b in { (still_not-bound_in p) where p is Element of CQC-WFF Al : p in X } by TARSKI:def 4;
ex p being Element of CQC-WFF Al st
( b = still_not-bound_in p & p in X ) by A3;
then b in { (still_not-bound_in q) where q is Element of CQC-WFF Al : q in Y } by A1;
hence a in still_not-bound_in Y by A2, TARSKI:def 4; :: thesis: verum