let A be QC-alphabet ; :: thesis: for p being Element of QC-WFF A st p is universal holds
p = All ((bound_in p),(the_scope_of p))
let p be Element of QC-WFF A; :: thesis: ( p is universal implies p = All ((bound_in p),(the_scope_of p)) )
given x being bound_QC-variable of A, q being Element of QC-WFF A such that A1: p = All (x,q) ; :: according to QC_LANG1:def 21 :: thesis: p = All ((bound_in p),(the_scope_of p))
A2: p is universal by A1, QC_LANG1:def 21;
then x = bound_in p by A1, QC_LANG1:def 27;
hence p = All ((bound_in p),(the_scope_of p)) by A1, A2, QC_LANG1:def 28; :: thesis: verum