let p, q be Element of CQC-WFF ; :: thesis: ( p is_an_universal_closure_of q implies p |-| q )
assume p is_an_universal_closure_of q ; :: thesis: p |-| q
then consider n being Element of NAT such that
A1: ( 1 <= n & ex L being FinSequence st
( len L = n & L . 1 = q & L . n = p & ( for k being Element of NAT st 1 <= k & k < n holds
ex x being bound_QC-variable ex r being Element of CQC-WFF st
( r = L . k & L . (k + 1) = All x,r ) ) ) ) by Def6;
consider L being FinSequence such that
len L = n and
A2: L . 1 = q and
A3: L . n = p and
A4: for k being Element of NAT st 1 <= k & k < n holds
ex x being bound_QC-variable ex r being Element of CQC-WFF st
( r = L . k & L . (k + 1) = All x,r ) by A1;
for k being Element of NAT st 1 <= k & k <= n holds
ex r being Element of CQC-WFF st
( r = L . k & q |-| r )

proof

defpred S₁[ Element of NAT ] means ( 1 <= $1 & $1 <= n implies ex r being Element of CQC-WFF st
( r = L . $1 & q |-| r ) );
A5: S₁[ 0 ] ;
A6: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[k + 1]

now

assume that
1 <= k + 1 and
A8: k + 1 <= n ; :: thesis: ( ( k = 0 & ex p, r being Element of CQC-WFF st
( r = L . (k + 1) & q |-| r ) ) or ( 1 <= k & k < n & ex s being Element of CQC-WFF st
( s = L . (k + 1) & q |-| s ) ) )

per cases ( k = 0 or ( 1 <= k & k < n ) ) by A8, NAT_1:13, NAT_1:14;

case A9: k = 0 ; :: thesis: ex p, r being Element of CQC-WFF st
( r = L . (k + 1) & q |-| r )

take p = q; :: thesis: ex r being Element of CQC-WFF st
( r = L . (k + 1) & q |-| r )
thus ex r being Element of CQC-WFF st
( r = L . (k + 1) & q |-| r ) by A2, A9; :: thesis: verum

end;

case A10: ( 1 <= k & k < n ) ; :: thesis: ex s being Element of CQC-WFF st
( s = L . (k + 1) & q |-| s )

then consider x being bound_QC-variable, r being Element of CQC-WFF such that
A11: r = L . k and
A12: L . (k + 1) = All x,r by A4;
consider s being Element of CQC-WFF such that
A13: s = All x,r ;
s |-| r by A13, Th36;
hence ex s being Element of CQC-WFF st
( s = L . (k + 1) & q |-| s ) by A7, A10, A11, A12, A13, Th28; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A5, A6); :: thesis: verum

end;

then ex r being Element of CQC-WFF st
( r = L . n & q |-| r ) by A1;
hence p |-| q by A3; :: thesis: verum