let x be bound_QC-variable; :: thesis: for p being QC-formula st p is closed holds
All x,p is closed
let p be QC-formula; :: thesis: ( p is closed implies All x,p is closed )
assume still_not-bound_in p = {} ; :: according to QC_LANG1:def 30 :: 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 Th27; :: thesis: verum