:: deftheorem defines is_an_universal_closure_of CQC_THE3:def 6 :
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( p is_an_universal_closure_of q iff ( p is closed & ex n being Element of NAT st
( 1 <= n & ex L being FinSequence st
( len L = n & L . 1 = q & L . n = p & ( for k being Nat st 1 <= k & k < n holds
ex x being bound_QC-variable of A ex r being Element of CQC-WFF A st
( r = L . k & L . (k + 1) = All (x,r) ) ) ) ) ) );