let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A st p is_an_universal_closure_of q holds
p |-| q
let p, q be Element of CQC-WFF A; :: 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 and
A2: 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) ) ) ) ;
consider L being FinSequence such that
len L = n and
A3: L . 1 = q and
A4: L . n = p and
A5: 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) ) by A2;
for k being Nat st 1 <= k & k <= n holds
ex r being Element of CQC-WFF A st
( r = L . k & q |-| r )
proof
defpred S1[ Nat] means ( 1 <= $1 & $1 <= n implies ex r being Element of CQC-WFF A st
( r = L . $1 & q |-| r ) );
A6: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A7: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: ( 1 <= k + 1 & k + 1 <= n & not ( k = 0 & ex p, r being Element of CQC-WFF A st
( r = L . (k + 1) & q |-| r ) ) implies ( 1 <= k & k < n & ex s being Element of CQC-WFF A st
( s = L . (k + 1) & q |-| s ) ) )
assume that
1 <= k + 1 and
A8: k + 1 <= n ; :: thesis: ( ( k = 0 & ex p, r being Element of CQC-WFF A st
( r = L . (k + 1) & q |-| r ) ) or ( 1 <= k & k < n & ex s being Element of CQC-WFF A 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 A st
( r = L . (k + 1) & q |-| r )
take p = q; :: thesis: ex r being Element of CQC-WFF A st
( r = L . (k + 1) & q |-| r )
thus ex r being Element of CQC-WFF A st
( r = L . (k + 1) & q |-| r ) by A3, A9; :: thesis: verum
end;
case A10: ( 1 <= k & k < n ) ; :: thesis: ex s being Element of CQC-WFF A st
( s = L . (k + 1) & q |-| s )
then consider x being bound_QC-variable of A, r being Element of CQC-WFF A such that
A11: r = L . k and
A12: L . (k + 1) = All (x,r) by A5;
consider s being Element of CQC-WFF A such that
A13: s = All (x,r) ;
s |-| r by A13, Th36;
hence ex s being Element of CQC-WFF A st
( s = L . (k + 1) & q |-| s ) by A7, A10, A11, A12, A13, Th28; :: thesis: verum
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
A14: S1[ 0 ] ;
thus for k being Nat holds S1[k] from NAT_1:sch 2(A14, A6); :: thesis: verum
end;
then ex r being Element of CQC-WFF A st
( r = L . n & q |-| r ) by A1;
hence p |-| q by A4; :: thesis: verum