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