let A be QC-alphabet ; :: thesis: for x being bound_QC-variable of A
for p being QC-formula of A st p is closed holds
All (x,p) is closed
let x be bound_QC-variable of A; :: thesis: for p being QC-formula of A st p is closed holds
All (x,p) is closed
let p be QC-formula of A; :: thesis: ( p is closed implies All (x,p) is closed )
assume still_not-bound_in p = {} ; :: according to QC_LANG1:def 31 :: thesis: All (x,p) is closed
then still_not-bound_in p c= {x} by XBOOLE_1:2;
hence All (x,p) is closed by Th23; :: thesis: verum