let Al be QC-alphabet ; :: thesis: for PHI being Consistent Subset of (CQC-WFF Al) ex Al2 being Al -expanding QC-alphabet ex PSI being Consistent Subset of (CQC-WFF Al2) st

( PHI c= PSI & PSI is with_examples )

let PHI be Consistent Subset of (CQC-WFF Al); :: thesis: ex Al2 being Al -expanding QC-alphabet ex PSI being Consistent Subset of (CQC-WFF Al2) st

( PHI c= PSI & PSI is with_examples )

deffunc H_{1}( Nat) -> Al -expanding QC-alphabet = $1 -th_FCEx Al;

deffunc H_{2}( Nat) -> Subset of (CQC-WFF ($1 -th_FCEx Al)) = $1 -th_EF (Al,PHI);

set Al2 = union { H_{1}(n) where n is Element of NAT : verum } ;

set PSI = union { H_{2}(n) where n is Element of NAT : verum } ;

A1: PHI c= union { H_{2}(n) where n is Element of NAT : verum }
_{1}(n) where n is Element of NAT : verum } & ( for n being Element of NAT holds H_{1}(n) c= union { H_{1}(n) where n is Element of NAT : verum } ) )
_{1}(n) where n is Element of NAT : verum } as non empty set by A2;

set Al2sym = union { (QC-symbols H_{1}(n)) where n is Element of NAT : verum } ;

( NAT c= union { (QC-symbols H_{1}(n)) where n is Element of NAT : verum } & Al2 = [:NAT,(union { (QC-symbols H_{1}(n)) where n is Element of NAT : verum } ):] )

reconsider Al2 = Al2 as Al -expanding QC-alphabet by A2, QC_TRANS:def 1;

for p being object st p in union { H_{2}(n) where n is Element of NAT : verum } holds

p in CQC-WFF Al2_{2}(n) where n is Element of NAT : verum } as Subset of (CQC-WFF Al2) by TARSKI:def 3;

PSI is Consistent

set S = { H_{1}(n) where n is Element of NAT : verum } ;

H_{1}( 0 ) in { H_{1}(n) where n is Element of NAT : verum }
;

then reconsider S = { H_{1}(n) where n is Element of NAT : verum } as non empty set ;

A39: for a, b being set st a in S & b in S holds

ex c being set st

( a \/ b c= c & c in S )_{1}(n)

( PHI c= PSI & PSI is with_examples ) by A1; :: thesis: verum

( PHI c= PSI & PSI is with_examples )

let PHI be Consistent Subset of (CQC-WFF Al); :: thesis: ex Al2 being Al -expanding QC-alphabet ex PSI being Consistent Subset of (CQC-WFF Al2) st

( PHI c= PSI & PSI is with_examples )

deffunc H

deffunc H

set Al2 = union { H

set PSI = union { H

A1: PHI c= union { H

proof

A2:
( Al c= union { H
PHI = H_{2}( 0 )
by Def9;

then PHI in { H_{2}(n) where n is Element of NAT : verum }
;

hence PHI c= union { H_{2}(n) where n is Element of NAT : verum }
by ZFMISC_1:74; :: thesis: verum

end;then PHI in { H

hence PHI c= union { H

proof

reconsider Al2 = union { H
Al = H_{1}( 0 )
by Def7;

then Al in { H_{1}(n) where n is Element of NAT : verum }
;

hence Al c= union { H_{1}(n) where n is Element of NAT : verum }
by ZFMISC_1:74; :: thesis: for n being Element of NAT holds H_{1}(n) c= union { H_{1}(n) where n is Element of NAT : verum }

let n be Element of NAT ; :: thesis: H_{1}(n) c= union { H_{1}(n) where n is Element of NAT : verum }

H_{1}(n) in { H_{1}(k) where k is Element of NAT : verum }
;

hence H_{1}(n) c= union { H_{1}(n) where n is Element of NAT : verum }
by ZFMISC_1:74; :: thesis: verum

end;then Al in { H

hence Al c= union { H

let n be Element of NAT ; :: thesis: H

H

hence H

set Al2sym = union { (QC-symbols H

( NAT c= union { (QC-symbols H

proof

then reconsider Al2 = Al2 as QC-alphabet by QC_LANG1:def 1;
for s being object st s in Al2 holds

s in [:NAT,(union { (QC-symbols H_{1}(n)) where n is Element of NAT : verum } ):]
_{1}(n)) where n is Element of NAT : verum } ):]
;

QC-symbols Al = QC-symbols H_{1}( 0 )
by Def7;

then QC-symbols Al in { (QC-symbols H_{1}(n)) where n is Element of NAT : verum }
;

then ( NAT c= QC-symbols Al & QC-symbols Al c= union { (QC-symbols H_{1}(n)) where n is Element of NAT : verum } )
by QC_LANG1:3, ZFMISC_1:74;

hence NAT c= union { (QC-symbols H_{1}(n)) where n is Element of NAT : verum }
; :: thesis: Al2 = [:NAT,(union { (QC-symbols H_{1}(n)) where n is Element of NAT : verum } ):]

for x being object st x in [:NAT,(union { (QC-symbols H_{1}(n)) where n is Element of NAT : verum } ):] holds

x in Al2_{1}(n)) where n is Element of NAT : verum } ):] c= Al2
;

hence Al2 = [:NAT,(union { (QC-symbols H_{1}(n)) where n is Element of NAT : verum } ):]
by A8, XBOOLE_0:def 10; :: thesis: verum

end;s in [:NAT,(union { (QC-symbols H

proof

then A8:
Al2 c= [:NAT,(union { (QC-symbols H
let s be object ; :: thesis: ( s in Al2 implies s in [:NAT,(union { (QC-symbols H_{1}(n)) where n is Element of NAT : verum } ):] )

assume A3: s in Al2 ; :: thesis: s in [:NAT,(union { (QC-symbols H_{1}(n)) where n is Element of NAT : verum } ):]

consider P being set such that

A4: ( s in P & P in { H_{1}(n) where n is Element of NAT : verum } )
by A3, TARSKI:def 4;

consider n being Element of NAT such that

A5: P = H_{1}(n)
by A4;

A6: for y being set st y in QC-symbols H_{1}(n) holds

y in union { (QC-symbols H_{1}(n)) where n is Element of NAT : verum }
_{1}(n)):]
by A5, A4, QC_LANG1:5;

then ex k, y being object st

( k in NAT & y in QC-symbols H_{1}(n) & s = [k,y] )
by ZFMISC_1:def 2;

then ex k, y being set st

( k in NAT & y in union { (QC-symbols H_{1}(n)) where n is Element of NAT : verum } & s = [k,y] )
by A6;

hence s in [:NAT,(union { (QC-symbols H_{1}(n)) where n is Element of NAT : verum } ):]
by ZFMISC_1:87; :: thesis: verum

end;assume A3: s in Al2 ; :: thesis: s in [:NAT,(union { (QC-symbols H

consider P being set such that

A4: ( s in P & P in { H

consider n being Element of NAT such that

A5: P = H

A6: for y being set st y in QC-symbols H

y in union { (QC-symbols H

proof

s in [:NAT,(QC-symbols H
let y be set ; :: thesis: ( y in QC-symbols H_{1}(n) implies y in union { (QC-symbols H_{1}(n)) where n is Element of NAT : verum } )

assume A7: y in QC-symbols H_{1}(n)
; :: thesis: y in union { (QC-symbols H_{1}(n)) where n is Element of NAT : verum }

QC-symbols H_{1}(n) in { (QC-symbols H_{1}(k)) where k is Element of NAT : verum }
;

hence y in union { (QC-symbols H_{1}(n)) where n is Element of NAT : verum }
by A7, TARSKI:def 4; :: thesis: verum

end;assume A7: y in QC-symbols H

QC-symbols H

hence y in union { (QC-symbols H

then ex k, y being object st

( k in NAT & y in QC-symbols H

then ex k, y being set st

( k in NAT & y in union { (QC-symbols H

hence s in [:NAT,(union { (QC-symbols H

QC-symbols Al = QC-symbols H

then QC-symbols Al in { (QC-symbols H

then ( NAT c= QC-symbols Al & QC-symbols Al c= union { (QC-symbols H

hence NAT c= union { (QC-symbols H

for x being object st x in [:NAT,(union { (QC-symbols H

x in Al2

proof

then
[:NAT,(union { (QC-symbols H
let x be object ; :: thesis: ( x in [:NAT,(union { (QC-symbols H_{1}(n)) where n is Element of NAT : verum } ):] implies x in Al2 )

assume A9: x in [:NAT,(union { (QC-symbols H_{1}(n)) where n is Element of NAT : verum } ):]
; :: thesis: x in Al2

consider m, y being object such that

A10: ( m in NAT & y in union { (QC-symbols H_{1}(n)) where n is Element of NAT : verum } & x = [m,y] )
by A9, ZFMISC_1:def 2;

consider P being set such that

A11: ( y in P & P in { (QC-symbols H_{1}(n)) where n is Element of NAT : verum } )
by A10, TARSKI:def 4;

consider n being Element of NAT such that

A12: P = QC-symbols H_{1}(n)
by A11;

[m,y] in [:NAT,(QC-symbols H_{1}(n)):]
by A10, A11, A12, ZFMISC_1:87;

then A13: [m,y] in H_{1}(n)
by QC_LANG1:5;

H_{1}(n) c= Al2
by A2;

hence x in Al2 by A10, A13; :: thesis: verum

end;assume A9: x in [:NAT,(union { (QC-symbols H

consider m, y being object such that

A10: ( m in NAT & y in union { (QC-symbols H

consider P being set such that

A11: ( y in P & P in { (QC-symbols H

consider n being Element of NAT such that

A12: P = QC-symbols H

[m,y] in [:NAT,(QC-symbols H

then A13: [m,y] in H

H

hence x in Al2 by A10, A13; :: thesis: verum

hence Al2 = [:NAT,(union { (QC-symbols H

reconsider Al2 = Al2 as Al -expanding QC-alphabet by A2, QC_TRANS:def 1;

for p being object st p in union { H

p in CQC-WFF Al2

proof

then reconsider PSI = union { H
let p be object ; :: thesis: ( p in union { H_{2}(n) where n is Element of NAT : verum } implies p in CQC-WFF Al2 )

assume A14: p in union { H_{2}(n) where n is Element of NAT : verum }
; :: thesis: p in CQC-WFF Al2

consider P being set such that

A15: ( p in P & P in { H_{2}(n) where n is Element of NAT : verum } )
by A14, TARSKI:def 4;

consider n being Element of NAT such that

A16: P = H_{2}(n)
by A15;

Al2 is H_{1}(n) -expanding QC-alphabet
by A2, QC_TRANS:def 1;

then p is Element of CQC-WFF Al2 by QC_TRANS:7, A15, A16;

hence p in CQC-WFF Al2 ; :: thesis: verum

end;assume A14: p in union { H

consider P being set such that

A15: ( p in P & P in { H

consider n being Element of NAT such that

A16: P = H

Al2 is H

then p is Element of CQC-WFF Al2 by QC_TRANS:7, A15, A16;

hence p in CQC-WFF Al2 ; :: thesis: verum

PSI is Consistent

proof

then reconsider PSI = PSI as Consistent Subset of (CQC-WFF Al2) ;
defpred S_{1}[ Nat] means ( H_{2}($1) is Consistent & H_{2}($1) is Al2 -Consistent );

A17: S_{1}[ 0 ]
_{1}[n] holds

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(A17, A19);

A22: for n being Element of NAT holds H_{2}(n) c= PSI
_{2}(n) in bool (CQC-WFF Al2)

A25: ( dom f = NAT & ( for n being Element of NAT holds f . n = H_{2}(n) ) )
from FUNCT_1:sch 4();

for y being object st y in rng f holds

y in bool (CQC-WFF Al2)

set PSIp = union (rng f);

f in Funcs (NAT,(bool (CQC-WFF Al2))) by FUNCT_2:8;

then union (rng f) c= union (bool (CQC-WFF Al2)) by ZFMISC_1:77, FUNCT_2:92;

then reconsider PSIp = union (rng f) as Subset of (CQC-WFF Al2) by ZFMISC_1:81;

for n, m being Nat st m in dom f & n in dom f & n < m holds

( f . n is Consistent & f . n c= f . m )

for y being object st y in { H_{2}(n) where n is Element of NAT : verum } holds

ex x being object st

( x in dom f & y = f . x )_{2}(n) where n is Element of NAT : verum } c= rng f
by FUNCT_1:9;

for y being object st y in rng f holds

y in { H_{2}(n) where n is Element of NAT : verum }
_{2}(n) where n is Element of NAT : verum }
;

then PSIp = PSI by A36, XBOOLE_0:def 10;

hence PSI is Consistent ; :: thesis: verum

end;A17: S

proof

A19:
for n being Nat st S
A18:
H_{2}( 0 ) = PHI
by Def9;

PHI is Al2 -Consistent by QC_TRANS:23;

then ( H_{1}( 0 ) = Al & ( for S being Subset of (CQC-WFF Al2) st H_{2}( 0 ) = S holds

S is Consistent ) ) by A18, Def7, QC_TRANS:def 2;

hence S_{1}[ 0 ]
by A18, QC_TRANS:def 2; :: thesis: verum

end;PHI is Al2 -Consistent by QC_TRANS:23;

then ( H

S is Consistent ) ) by A18, Def7, QC_TRANS:def 2;

hence S

S

proof

A21:
for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

A20: FCEx H_{1}(n) = H_{1}(n + 1)
by Th5;

reconsider Al2 = Al2 as H_{1}(n + 1) -expanding QC-alphabet by A2, QC_TRANS:def 1;

assume S_{1}[n]
; :: thesis: S_{1}[n + 1]

then reconsider PSIn = H_{2}(n) as Consistent Subset of (CQC-WFF H_{1}(n)) ;

H_{2}(n + 1) = PSIn \/ (Example_Formulae_of H_{1}(n))
by Def9;

then reconsider PSIn1 = H_{2}(n + 1) as Consistent Subset of (CQC-WFF H_{1}(n + 1)) by A20, Th9;

PSIn1 is Al2 -Consistent by QC_TRANS:23;

hence S_{1}[n + 1]
; :: thesis: verum

end;A20: FCEx H

reconsider Al2 = Al2 as H

assume S

then reconsider PSIn = H

H

then reconsider PSIn1 = H

PSIn1 is Al2 -Consistent by QC_TRANS:23;

hence S

A22: for n being Element of NAT holds H

proof

A24:
for n being Element of NAT holds H
let n be Element of NAT ; :: thesis: H_{2}(n) c= PSI

let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in H_{2}(n) or p in PSI )

assume A23: p in H_{2}(n)
; :: thesis: p in PSI

H_{2}(n) in { H_{2}(k) where k is Element of NAT : verum }
;

hence p in PSI by A23, TARSKI:def 4; :: thesis: verum

end;let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in H

assume A23: p in H

H

hence p in PSI by A23, TARSKI:def 4; :: thesis: verum

proof

consider f being Function such that
let n be Element of NAT ; :: thesis: H_{2}(n) in bool (CQC-WFF Al2)

( H_{2}(n) c= PSI & PSI c= CQC-WFF Al2 )
by A22;

then H_{2}(n) c= CQC-WFF Al2
;

hence H_{2}(n) in bool (CQC-WFF Al2)
; :: thesis: verum

end;( H

then H

hence H

A25: ( dom f = NAT & ( for n being Element of NAT holds f . n = H

for y being object st y in rng f holds

y in bool (CQC-WFF Al2)

proof

then reconsider f = f as sequence of (bool (CQC-WFF Al2)) by A25, FUNCT_2:2, TARSKI:def 3;
let y be object ; :: thesis: ( y in rng f implies y in bool (CQC-WFF Al2) )

assume A26: y in rng f ; :: thesis: y in bool (CQC-WFF Al2)

consider x being object such that

A27: ( x in dom f & y = f . x ) by A26, FUNCT_1:def 3;

reconsider x = x as Element of NAT by A25, A27;

f . x = H_{2}(x)
by A25;

hence y in bool (CQC-WFF Al2) by A24, A27; :: thesis: verum

end;assume A26: y in rng f ; :: thesis: y in bool (CQC-WFF Al2)

consider x being object such that

A27: ( x in dom f & y = f . x ) by A26, FUNCT_1:def 3;

reconsider x = x as Element of NAT by A25, A27;

f . x = H

hence y in bool (CQC-WFF Al2) by A24, A27; :: thesis: verum

set PSIp = union (rng f);

f in Funcs (NAT,(bool (CQC-WFF Al2))) by FUNCT_2:8;

then union (rng f) c= union (bool (CQC-WFF Al2)) by ZFMISC_1:77, FUNCT_2:92;

then reconsider PSIp = union (rng f) as Subset of (CQC-WFF Al2) by ZFMISC_1:81;

for n, m being Nat st m in dom f & n in dom f & n < m holds

( f . n is Consistent & f . n c= f . m )

proof

then reconsider PSIp = PSIp as Consistent Subset of (CQC-WFF Al2) by HENMODEL:11;
let nn, mm be Nat; :: thesis: ( mm in dom f & nn in dom f & nn < mm implies ( f . nn is Consistent & f . nn c= f . mm ) )

assume A28: ( mm in dom f & nn in dom f & nn < mm ) ; :: thesis: ( f . nn is Consistent & f . nn c= f . mm )

reconsider n = nn, m = mm as Element of NAT by ORDINAL1:def 12;

( f . n is Subset of (CQC-WFF Al2) & f . n = H_{2}(n) & H_{2}(n) is Al2 -Consistent )
by A21, A25;

hence f . nn is Consistent by QC_TRANS:def 2; :: thesis: f . nn c= f . mm

defpred S_{2}[ Nat] means ( $1 <= m implies ex k being Element of NAT st

( k = m - $1 & H_{2}(k) c= H_{2}(m) ) );

A29: S_{2}[ 0 ]
;

A30: for k being Nat st S_{2}[k] holds

S_{2}[k + 1]
_{2}[k]
from NAT_1:sch 2(A29, A30);

set k = m - n;

reconsider k = m - n as Element of NAT by A28, NAT_1:21;

( S_{2}[k] & k <= k + n )
by A33, NAT_1:11;

then ( H_{2}(n) c= H_{2}(m) & f . n = H_{2}(n) & f . m = H_{2}(m) )
by A25;

hence f . nn c= f . mm ; :: thesis: verum

end;assume A28: ( mm in dom f & nn in dom f & nn < mm ) ; :: thesis: ( f . nn is Consistent & f . nn c= f . mm )

reconsider n = nn, m = mm as Element of NAT by ORDINAL1:def 12;

( f . n is Subset of (CQC-WFF Al2) & f . n = H

hence f . nn is Consistent by QC_TRANS:def 2; :: thesis: f . nn c= f . mm

defpred S

( k = m - $1 & H

A29: S

A30: for k being Nat st S

S

proof

A33:
for k being Nat holds S
let k be Nat; :: thesis: ( S_{2}[k] implies S_{2}[k + 1] )

assume A31: S_{2}[k]
; :: thesis: S_{2}[k + 1]

set j1 = m - k;

set j2 = m - (k + 1);

end;assume A31: S

set j1 = m - k;

set j2 = m - (k + 1);

per cases
( k + 1 <= m or not k + 1 <= m )
;

end;

suppose A32:
k + 1 <= m
; :: thesis: S_{2}[k + 1]

then
k <= m
by NAT_1:13;

then reconsider j1 = m - k, j2 = m - (k + 1) as Element of NAT by A32, NAT_1:21;

H_{2}(j2 + 1) = ( the EF-Sequence of Al,PHI . j2) \/ (Example_Formulae_of (j2 -th_FCEx Al))
by Def9;

then ( H_{2}(j2) c= H_{2}(j1) & H_{2}(j1) c= H_{2}(m) )
by A31, A32, NAT_1:13, XBOOLE_1:7;

hence S_{2}[k + 1]
by XBOOLE_1:1; :: thesis: verum

end;then reconsider j1 = m - k, j2 = m - (k + 1) as Element of NAT by A32, NAT_1:21;

H

then ( H

hence S

set k = m - n;

reconsider k = m - n as Element of NAT by A28, NAT_1:21;

( S

then ( H

hence f . nn c= f . mm ; :: thesis: verum

for y being object st y in { H

ex x being object st

( x in dom f & y = f . x )

proof

then A36:
{ H
let P be object ; :: thesis: ( P in { H_{2}(n) where n is Element of NAT : verum } implies ex x being object st

( x in dom f & P = f . x ) )

assume A34: P in { H_{2}(n) where n is Element of NAT : verum }
; :: thesis: ex x being object st

( x in dom f & P = f . x )

consider n being Element of NAT such that

A35: P = H_{2}(n)
by A34;

( n in dom f & f . n = P ) by A25, A35;

hence ex x being object st

( x in dom f & P = f . x ) ; :: thesis: verum

end;( x in dom f & P = f . x ) )

assume A34: P in { H

( x in dom f & P = f . x )

consider n being Element of NAT such that

A35: P = H

( n in dom f & f . n = P ) by A25, A35;

hence ex x being object st

( x in dom f & P = f . x ) ; :: thesis: verum

for y being object st y in rng f holds

y in { H

proof

then
rng f c= { H
let y be object ; :: thesis: ( y in rng f implies y in { H_{2}(n) where n is Element of NAT : verum } )

assume A37: y in rng f ; :: thesis: y in { H_{2}(n) where n is Element of NAT : verum }

consider x being object such that

A38: ( x in dom f & y = f . x ) by A37, FUNCT_1:def 3;

reconsider x = x as Element of NAT by A25, A38;

f . x = H_{2}(x)
by A25;

hence y in { H_{2}(n) where n is Element of NAT : verum }
by A38; :: thesis: verum

end;assume A37: y in rng f ; :: thesis: y in { H

consider x being object such that

A38: ( x in dom f & y = f . x ) by A37, FUNCT_1:def 3;

reconsider x = x as Element of NAT by A25, A38;

f . x = H

hence y in { H

then PSIp = PSI by A36, XBOOLE_0:def 10;

hence PSI is Consistent ; :: thesis: verum

set S = { H

H

then reconsider S = { H

A39: for a, b being set st a in S & b in S holds

ex c being set st

( a \/ b c= c & c in S )

proof

A43:
for p being Element of CQC-WFF Al2 ex n being Element of NAT st p is Element of CQC-WFF H
let a, b be set ; :: thesis: ( a in S & b in S implies ex c being set st

( a \/ b c= c & c in S ) )

assume A40: ( a in S & b in S ) ; :: thesis: ex c being set st

( a \/ b c= c & c in S )

consider i being Element of NAT such that

A41: a = H_{1}(i)
by A40;

consider j being Element of NAT such that

A42: b = H_{1}(j)
by A40;

end;( a \/ b c= c & c in S ) )

assume A40: ( a in S & b in S ) ; :: thesis: ex c being set st

( a \/ b c= c & c in S )

consider i being Element of NAT such that

A41: a = H

consider j being Element of NAT such that

A42: b = H

per cases
( j <= i or not j <= i )
;

end;

suppose
j <= i
; :: thesis: ex c being set st

( a \/ b c= c & c in S )

( a \/ b c= c & c in S )

then
H_{1}(j) c= H_{1}(i)
by Th6;

hence ex c being set st

( a \/ b c= c & c in S ) by A40, A41, A42, XBOOLE_1:8; :: thesis: verum

end;hence ex c being set st

( a \/ b c= c & c in S ) by A40, A41, A42, XBOOLE_1:8; :: thesis: verum

suppose
not j <= i
; :: thesis: ex c being set st

( a \/ b c= c & c in S )

( a \/ b c= c & c in S )

then
H_{1}(i) c= H_{1}(j)
by Th6;

hence ex c being set st

( a \/ b c= c & c in S ) by A40, A41, A42, XBOOLE_1:8; :: thesis: verum

end;hence ex c being set st

( a \/ b c= c & c in S ) by A40, A41, A42, XBOOLE_1:8; :: thesis: verum

proof

PSI is with_examples
defpred S_{1}[ Element of CQC-WFF Al2] means ex n being Element of NAT st $1 is Element of CQC-WFF H_{1}(n);

A44: S_{1}[ VERUM Al2]

for P being QC-pred_symbol of k,Al2

for l being CQC-variable_list of k,Al2 holds S_{1}[P ! l]
_{1}[r] holds

S_{1}[ 'not' r]
_{1}[r] & S_{1}[s] holds

S_{1}[r '&' s]

for r being Element of CQC-WFF Al2 st S_{1}[r] holds

S_{1}[ All (x,r)]

for x being bound_QC-variable of Al2

for k being Nat

for l being CQC-variable_list of k,Al2

for P being QC-pred_symbol of k,Al2 holds

( S_{1}[ VERUM Al2] & S_{1}[P ! l] & ( S_{1}[r] implies S_{1}[ 'not' r] ) & ( S_{1}[r] & S_{1}[s] implies S_{1}[r '&' s] ) & ( S_{1}[r] implies S_{1}[ All (x,r)] ) )
by A44, A45, A59, A62;

for p being Element of CQC-WFF Al2 holds S_{1}[p]
from CQC_LANG:sch 1(A80);

hence for p being Element of CQC-WFF Al2 ex n being Element of NAT st p is Element of CQC-WFF H_{1}(n)
; :: thesis: verum

end;A44: S

proof

A45:
for k being Nat
reconsider Al2 = Al2 as H_{1}( 0 ) -expanding QC-alphabet by A2, QC_TRANS:def 1;

VERUM H_{1}( 0 ) in CQC-WFF H_{1}( 0 )
;

then Al2 -Cast (VERUM H_{1}( 0 )) in CQC-WFF H_{1}( 0 )
by QC_TRANS:def 3;

then VERUM Al2 in CQC-WFF H_{1}( 0 )
by QC_TRANS:8;

hence S_{1}[ VERUM Al2]
; :: thesis: verum

end;VERUM H

then Al2 -Cast (VERUM H

then VERUM Al2 in CQC-WFF H

hence S

for P being QC-pred_symbol of k,Al2

for l being CQC-variable_list of k,Al2 holds S

proof

A59:
for r being Element of CQC-WFF Al2 st S
let k be Nat; :: thesis: for P being QC-pred_symbol of k,Al2

for l being CQC-variable_list of k,Al2 holds S_{1}[P ! l]

let P be QC-pred_symbol of k,Al2; :: thesis: for l being CQC-variable_list of k,Al2 holds S_{1}[P ! l]

let l be CQC-variable_list of k,Al2; :: thesis: S_{1}[P ! l]

ex n being Element of NAT st

( rng l c= bound_QC-variables H_{1}(n) & P is QC-pred_symbol of k,H_{1}(n) )

A56: ( rng l c= bound_QC-variables H_{1}(n) & P is QC-pred_symbol of k,H_{1}(n) )
;

l is CQC-variable_list of k,H_{1}(n)
by A56, FINSEQ_1:def 4, XBOOLE_1:1;

then consider l2 being CQC-variable_list of k,H_{1}(n), P2 being QC-pred_symbol of k,H_{1}(n) such that

A57: ( l2 = l & P = P2 ) by A56;

reconsider Al2 = Al2 as H_{1}(n) -expanding QC-alphabet by A2, QC_TRANS:def 1;

A58: ( Al2 -Cast P2 = P & Al2 -Cast l2 = l ) by A57, QC_TRANS:def 5, QC_TRANS:def 6;

P2 ! l2 = Al2 -Cast (P2 ! l2) by QC_TRANS:def 3

.= P ! l by A58, QC_TRANS:8 ;

hence S_{1}[P ! l]
; :: thesis: verum

end;for l being CQC-variable_list of k,Al2 holds S

let P be QC-pred_symbol of k,Al2; :: thesis: for l being CQC-variable_list of k,Al2 holds S

let l be CQC-variable_list of k,Al2; :: thesis: S

ex n being Element of NAT st

( rng l c= bound_QC-variables H

proof

then consider n being Element of NAT such that
A46:
( rng l c= bound_QC-variables Al2 & {P} c= QC-pred_symbols Al2 )
by ZFMISC_1:31;

( bound_QC-variables Al2 c= QC-variables Al2 & QC-variables Al2 c= [:NAT,(QC-symbols Al2):] ) by QC_LANG1:4;

then A47: ( bound_QC-variables Al2 c= [:NAT,(QC-symbols Al2):] & QC-pred_symbols Al2 c= [:NAT,(QC-symbols Al2):] ) by QC_LANG1:6;

then ( rng l c= [:NAT,(QC-symbols Al2):] & {P} c= [:NAT,(QC-symbols Al2):] ) by A46;

then ( rng l c= Al2 & {P} c= Al2 ) by QC_LANG1:5;

then ( (rng l) \/ {P} c= union S & (rng l) \/ {P} is finite ) by XBOOLE_1:8;

then consider a being set such that

A48: ( a in S & (rng l) \/ {P} c= a ) by A39, COHSP_1:6, COHSP_1:13;

consider n being Element of NAT such that

A49: a = H_{1}(n)
by A48;

take n ; :: thesis: ( rng l c= bound_QC-variables H_{1}(n) & P is QC-pred_symbol of k,H_{1}(n) )

A50: ( rng l c= (rng l) \/ {P} & {P} c= (rng l) \/ {P} ) by XBOOLE_1:7;

for s being object st s in rng l holds

s in bound_QC-variables H_{1}(n)
_{1}(n)
; :: thesis: P is QC-pred_symbol of k,H_{1}(n)

thus P is QC-pred_symbol of k,H_{1}(n)
:: thesis: verum

end;( bound_QC-variables Al2 c= QC-variables Al2 & QC-variables Al2 c= [:NAT,(QC-symbols Al2):] ) by QC_LANG1:4;

then A47: ( bound_QC-variables Al2 c= [:NAT,(QC-symbols Al2):] & QC-pred_symbols Al2 c= [:NAT,(QC-symbols Al2):] ) by QC_LANG1:6;

then ( rng l c= [:NAT,(QC-symbols Al2):] & {P} c= [:NAT,(QC-symbols Al2):] ) by A46;

then ( rng l c= Al2 & {P} c= Al2 ) by QC_LANG1:5;

then ( (rng l) \/ {P} c= union S & (rng l) \/ {P} is finite ) by XBOOLE_1:8;

then consider a being set such that

A48: ( a in S & (rng l) \/ {P} c= a ) by A39, COHSP_1:6, COHSP_1:13;

consider n being Element of NAT such that

A49: a = H

take n ; :: thesis: ( rng l c= bound_QC-variables H

A50: ( rng l c= (rng l) \/ {P} & {P} c= (rng l) \/ {P} ) by XBOOLE_1:7;

for s being object st s in rng l holds

s in bound_QC-variables H

proof

hence
rng l c= bound_QC-variables H
let s be object ; :: thesis: ( s in rng l implies s in bound_QC-variables H_{1}(n) )

assume A51: s in rng l ; :: thesis: s in bound_QC-variables H_{1}(n)

s in bound_QC-variables Al2 by A51;

then s in [:{4},(QC-symbols Al2):] by QC_LANG1:def 4;

then consider s1, s2 being object such that

A52: ( s1 in {4} & s2 in QC-symbols Al2 & s = [s1,s2] ) by ZFMISC_1:def 2;

( rng l c= H_{1}(n) & {P} c= H_{1}(n) )
by A48, A49, A50;

then s in H_{1}(n)
by A51;

then s in [:NAT,(QC-symbols H_{1}(n)):]
by QC_LANG1:5;

then consider s3, s4 being object such that

A53: ( s3 in NAT & s4 in QC-symbols H_{1}(n) & s = [s3,s4] )
by ZFMISC_1:def 2;

s = [s1,s4] by A52, A53, XTUPLE_0:1;

then s in [:{4},(QC-symbols H_{1}(n)):]
by A52, A53, ZFMISC_1:def 2;

hence s in bound_QC-variables H_{1}(n)
by QC_LANG1:def 4; :: thesis: verum

end;assume A51: s in rng l ; :: thesis: s in bound_QC-variables H

s in bound_QC-variables Al2 by A51;

then s in [:{4},(QC-symbols Al2):] by QC_LANG1:def 4;

then consider s1, s2 being object such that

A52: ( s1 in {4} & s2 in QC-symbols Al2 & s = [s1,s2] ) by ZFMISC_1:def 2;

( rng l c= H

then s in H

then s in [:NAT,(QC-symbols H

then consider s3, s4 being object such that

A53: ( s3 in NAT & s4 in QC-symbols H

s = [s1,s4] by A52, A53, XTUPLE_0:1;

then s in [:{4},(QC-symbols H

hence s in bound_QC-variables H

thus P is QC-pred_symbol of k,H

proof

P in [:NAT,(QC-symbols Al2):]
by A47;

then consider p1, p2 being object such that

A54: ( p1 in NAT & p2 in QC-symbols Al2 & P = [p1,p2] ) by ZFMISC_1:def 2;

( rng l c= H_{1}(n) & P in H_{1}(n) )
by A48, A49, A50, ZFMISC_1:31;

then P in [:NAT,(QC-symbols H_{1}(n)):]
by QC_LANG1:5;

then reconsider p2 = p2 as QC-symbol of H_{1}(n) by A54, ZFMISC_1:87;

A55: P `1 = (the_arity_of P) + 7 by QC_LANG1:def 8

.= k + 7 by QC_LANG1:11 ;

reconsider p1 = p1 as Element of NAT by A54;

( P `1 = 7 + (the_arity_of P) & P `1 = p1 ) by A54, QC_LANG1:def 8;

then 7 <= p1 by NAT_1:11;

then [p1,p2] in { [m,x] where m is Nat, x is QC-symbol of H_{1}(n) : 7 <= m }
;

then reconsider P = P as QC-pred_symbol of H_{1}(n) by A54, QC_LANG1:def 7;

the_arity_of P = k by A55, QC_LANG1:def 8;

then P in { Q where Q is QC-pred_symbol of H_{1}(n) : the_arity_of Q = k }
;

hence P is QC-pred_symbol of k,H_{1}(n)
by QC_LANG1:def 9; :: thesis: verum

end;then consider p1, p2 being object such that

A54: ( p1 in NAT & p2 in QC-symbols Al2 & P = [p1,p2] ) by ZFMISC_1:def 2;

( rng l c= H

then P in [:NAT,(QC-symbols H

then reconsider p2 = p2 as QC-symbol of H

A55: P `1 = (the_arity_of P) + 7 by QC_LANG1:def 8

.= k + 7 by QC_LANG1:11 ;

reconsider p1 = p1 as Element of NAT by A54;

( P `1 = 7 + (the_arity_of P) & P `1 = p1 ) by A54, QC_LANG1:def 8;

then 7 <= p1 by NAT_1:11;

then [p1,p2] in { [m,x] where m is Nat, x is QC-symbol of H

then reconsider P = P as QC-pred_symbol of H

the_arity_of P = k by A55, QC_LANG1:def 8;

then P in { Q where Q is QC-pred_symbol of H

hence P is QC-pred_symbol of k,H

A56: ( rng l c= bound_QC-variables H

l is CQC-variable_list of k,H

then consider l2 being CQC-variable_list of k,H

A57: ( l2 = l & P = P2 ) by A56;

reconsider Al2 = Al2 as H

A58: ( Al2 -Cast P2 = P & Al2 -Cast l2 = l ) by A57, QC_TRANS:def 5, QC_TRANS:def 6;

P2 ! l2 = Al2 -Cast (P2 ! l2) by QC_TRANS:def 3

.= P ! l by A58, QC_TRANS:8 ;

hence S

S

proof

A62:
for r, s being Element of CQC-WFF Al2 st S
let r be Element of CQC-WFF Al2; :: thesis: ( S_{1}[r] implies S_{1}[ 'not' r] )

assume S_{1}[r]
; :: thesis: S_{1}[ 'not' r]

then consider n being Element of NAT such that

A60: r is Element of CQC-WFF H_{1}(n)
;

consider r2 being Element of CQC-WFF H_{1}(n) such that

A61: r = r2 by A60;

reconsider Al2 = Al2 as H_{1}(n) -expanding QC-alphabet by A2, QC_TRANS:def 1;

'not' r2 = Al2 -Cast ('not' r2) by QC_TRANS:def 3

.= 'not' (Al2 -Cast r2) by QC_TRANS:8

.= 'not' r by A61, QC_TRANS:def 3 ;

hence S_{1}[ 'not' r]
; :: thesis: verum

end;assume S

then consider n being Element of NAT such that

A60: r is Element of CQC-WFF H

consider r2 being Element of CQC-WFF H

A61: r = r2 by A60;

reconsider Al2 = Al2 as H

'not' r2 = Al2 -Cast ('not' r2) by QC_TRANS:def 3

.= 'not' (Al2 -Cast r2) by QC_TRANS:8

.= 'not' r by A61, QC_TRANS:def 3 ;

hence S

S

proof

for x being bound_QC-variable of Al2
let r, s be Element of CQC-WFF Al2; :: thesis: ( S_{1}[r] & S_{1}[s] implies S_{1}[r '&' s] )

assume ( S_{1}[r] & S_{1}[s] )
; :: thesis: S_{1}[r '&' s]

then consider n, m being Element of NAT such that

A63: ( r is Element of CQC-WFF H_{1}(n) & s is Element of CQC-WFF H_{1}(m) )
;

end;assume ( S

then consider n, m being Element of NAT such that

A63: ( r is Element of CQC-WFF H

per cases
( n <= m or not n <= m )
;

end;

suppose
n <= m
; :: thesis: S_{1}[r '&' s]

then reconsider Sm = H_{1}(m) as H_{1}(n) -expanding QC-alphabet by Th6, QC_TRANS:def 1;

r is Element of CQC-WFF Sm by A63, QC_TRANS:7;

then consider r2, s2 being Element of CQC-WFF Sm such that

A64: ( r2 = r & s2 = s ) by A63;

reconsider Al2 = Al2 as Sm -expanding QC-alphabet by A2, QC_TRANS:def 1;

A65: ( r = Al2 -Cast r2 & s = Al2 -Cast s2 ) by A64, QC_TRANS:def 3;

r2 '&' s2 = Al2 -Cast (r2 '&' s2) by QC_TRANS:def 3

.= r '&' s by A65, QC_TRANS:8 ;

hence S_{1}[r '&' s]
; :: thesis: verum

end;r is Element of CQC-WFF Sm by A63, QC_TRANS:7;

then consider r2, s2 being Element of CQC-WFF Sm such that

A64: ( r2 = r & s2 = s ) by A63;

reconsider Al2 = Al2 as Sm -expanding QC-alphabet by A2, QC_TRANS:def 1;

A65: ( r = Al2 -Cast r2 & s = Al2 -Cast s2 ) by A64, QC_TRANS:def 3;

r2 '&' s2 = Al2 -Cast (r2 '&' s2) by QC_TRANS:def 3

.= r '&' s by A65, QC_TRANS:8 ;

hence S

suppose
not n <= m
; :: thesis: S_{1}[r '&' s]

then reconsider Sn = H_{1}(n) as H_{1}(m) -expanding QC-alphabet by Th6, QC_TRANS:def 1;

s is Element of CQC-WFF Sn by A63, QC_TRANS:7;

then consider r2, s2 being Element of CQC-WFF Sn such that

A66: ( r2 = r & s2 = s ) by A63;

reconsider Al2 = Al2 as Sn -expanding QC-alphabet by A2, QC_TRANS:def 1;

A67: ( r = Al2 -Cast r2 & s = Al2 -Cast s2 ) by A66, QC_TRANS:def 3;

r2 '&' s2 = Al2 -Cast (r2 '&' s2) by QC_TRANS:def 3

.= r '&' s by A67, QC_TRANS:8 ;

hence S_{1}[r '&' s]
; :: thesis: verum

end;s is Element of CQC-WFF Sn by A63, QC_TRANS:7;

then consider r2, s2 being Element of CQC-WFF Sn such that

A66: ( r2 = r & s2 = s ) by A63;

reconsider Al2 = Al2 as Sn -expanding QC-alphabet by A2, QC_TRANS:def 1;

A67: ( r = Al2 -Cast r2 & s = Al2 -Cast s2 ) by A66, QC_TRANS:def 3;

r2 '&' s2 = Al2 -Cast (r2 '&' s2) by QC_TRANS:def 3

.= r '&' s by A67, QC_TRANS:8 ;

hence S

for r being Element of CQC-WFF Al2 st S

S

proof

then A80:
for r, s being Element of CQC-WFF Al2
let x be bound_QC-variable of Al2; :: thesis: for r being Element of CQC-WFF Al2 st S_{1}[r] holds

S_{1}[ All (x,r)]

let r be Element of CQC-WFF Al2; :: thesis: ( S_{1}[r] implies S_{1}[ All (x,r)] )

( x in QC-variables Al2 & QC-variables Al2 c= [:NAT,(QC-symbols Al2):] ) by QC_LANG1:4;

then ( x in [:NAT,(QC-symbols Al2):] & Al2 = [:NAT,(QC-symbols Al2):] ) by QC_LANG1:5;

then ( {x} c= union S & {x} is finite ) by ZFMISC_1:31;

then consider a being set such that

A68: ( a in S & {x} c= a ) by A39, COHSP_1:6, COHSP_1:13;

consider n being Element of NAT such that

A69: a = H_{1}(n)
by A68;

assume S_{1}[r]
; :: thesis: S_{1}[ All (x,r)]

then consider m being Element of NAT such that

A70: r is Element of CQC-WFF H_{1}(m)
;

x in bound_QC-variables Al2 ;

then x in [:{4},(QC-symbols Al2):] by QC_LANG1:def 4;

then consider x1, x2 being object such that

A71: ( x1 in {4} & x2 in QC-symbols Al2 & x = [x1,x2] ) by ZFMISC_1:def 2;

A72: x in H_{1}(n)
by A68, A69, ZFMISC_1:31;

end;S

let r be Element of CQC-WFF Al2; :: thesis: ( S

( x in QC-variables Al2 & QC-variables Al2 c= [:NAT,(QC-symbols Al2):] ) by QC_LANG1:4;

then ( x in [:NAT,(QC-symbols Al2):] & Al2 = [:NAT,(QC-symbols Al2):] ) by QC_LANG1:5;

then ( {x} c= union S & {x} is finite ) by ZFMISC_1:31;

then consider a being set such that

A68: ( a in S & {x} c= a ) by A39, COHSP_1:6, COHSP_1:13;

consider n being Element of NAT such that

A69: a = H

assume S

then consider m being Element of NAT such that

A70: r is Element of CQC-WFF H

x in bound_QC-variables Al2 ;

then x in [:{4},(QC-symbols Al2):] by QC_LANG1:def 4;

then consider x1, x2 being object such that

A71: ( x1 in {4} & x2 in QC-symbols Al2 & x = [x1,x2] ) by ZFMISC_1:def 2;

A72: x in H

per cases
( n <= m or not n <= m )
;

end;

suppose A73:
n <= m
; :: thesis: S_{1}[ All (x,r)]

then reconsider Sm = H_{1}(m) as H_{1}(n) -expanding QC-alphabet by Th6, QC_TRANS:def 1;

H_{1}(n) c= H_{1}(m)
by A73, Th6;

then x in H_{1}(m)
by A72;

then x in [:NAT,(QC-symbols H_{1}(m)):]
by QC_LANG1:5;

then consider x3, x4 being object such that

A74: ( x3 in NAT & x4 in QC-symbols H_{1}(m) & x = [x3,x4] )
by ZFMISC_1:def 2;

x = [x1,x4] by A71, A74, XTUPLE_0:1;

then x in [:{4},(QC-symbols Sm):] by A71, A74, ZFMISC_1:def 2;

then x is bound_QC-variable of Sm by QC_LANG1:def 4;

then consider x2 being bound_QC-variable of Sm, r2 being Element of CQC-WFF Sm such that

A75: ( x2 = x & r2 = r ) by A70;

reconsider Al2 = Al2 as Sm -expanding QC-alphabet by A2, QC_TRANS:def 1;

A76: ( r = Al2 -Cast r2 & x = Al2 -Cast x2 ) by A75, QC_TRANS:def 3, QC_TRANS:def 4;

All (x2,r2) = Al2 -Cast (All (x2,r2)) by QC_TRANS:def 3

.= All (x,r) by A76, QC_TRANS:8 ;

hence S_{1}[ All (x,r)]
; :: thesis: verum

end;H

then x in H

then x in [:NAT,(QC-symbols H

then consider x3, x4 being object such that

A74: ( x3 in NAT & x4 in QC-symbols H

x = [x1,x4] by A71, A74, XTUPLE_0:1;

then x in [:{4},(QC-symbols Sm):] by A71, A74, ZFMISC_1:def 2;

then x is bound_QC-variable of Sm by QC_LANG1:def 4;

then consider x2 being bound_QC-variable of Sm, r2 being Element of CQC-WFF Sm such that

A75: ( x2 = x & r2 = r ) by A70;

reconsider Al2 = Al2 as Sm -expanding QC-alphabet by A2, QC_TRANS:def 1;

A76: ( r = Al2 -Cast r2 & x = Al2 -Cast x2 ) by A75, QC_TRANS:def 3, QC_TRANS:def 4;

All (x2,r2) = Al2 -Cast (All (x2,r2)) by QC_TRANS:def 3

.= All (x,r) by A76, QC_TRANS:8 ;

hence S

suppose
not n <= m
; :: thesis: S_{1}[ All (x,r)]

then reconsider Sn = H_{1}(n) as H_{1}(m) -expanding QC-alphabet by Th6, QC_TRANS:def 1;

x in [:NAT,(QC-symbols Sn):] by A72, QC_LANG1:5;

then consider x3, x4 being object such that

A77: ( x3 in NAT & x4 in QC-symbols Sn & x = [x3,x4] ) by ZFMISC_1:def 2;

x = [x1,x4] by A71, A77, XTUPLE_0:1;

then x in [:{4},(QC-symbols Sn):] by A71, A77, ZFMISC_1:def 2;

then ( x is bound_QC-variable of Sn & r is Element of CQC-WFF Sn ) by A70, QC_TRANS:7, QC_LANG1:def 4;

then consider x2 being bound_QC-variable of Sn, r2 being Element of CQC-WFF Sn such that

A78: ( x2 = x & r2 = r ) ;

reconsider Al2 = Al2 as Sn -expanding QC-alphabet by A2, QC_TRANS:def 1;

A79: ( r = Al2 -Cast r2 & x = Al2 -Cast x2 ) by A78, QC_TRANS:def 3, QC_TRANS:def 4;

All (x2,r2) = Al2 -Cast (All (x2,r2)) by QC_TRANS:def 3

.= All (x,r) by A79, QC_TRANS:8 ;

hence S_{1}[ All (x,r)]
; :: thesis: verum

end;x in [:NAT,(QC-symbols Sn):] by A72, QC_LANG1:5;

then consider x3, x4 being object such that

A77: ( x3 in NAT & x4 in QC-symbols Sn & x = [x3,x4] ) by ZFMISC_1:def 2;

x = [x1,x4] by A71, A77, XTUPLE_0:1;

then x in [:{4},(QC-symbols Sn):] by A71, A77, ZFMISC_1:def 2;

then ( x is bound_QC-variable of Sn & r is Element of CQC-WFF Sn ) by A70, QC_TRANS:7, QC_LANG1:def 4;

then consider x2 being bound_QC-variable of Sn, r2 being Element of CQC-WFF Sn such that

A78: ( x2 = x & r2 = r ) ;

reconsider Al2 = Al2 as Sn -expanding QC-alphabet by A2, QC_TRANS:def 1;

A79: ( r = Al2 -Cast r2 & x = Al2 -Cast x2 ) by A78, QC_TRANS:def 3, QC_TRANS:def 4;

All (x2,r2) = Al2 -Cast (All (x2,r2)) by QC_TRANS:def 3

.= All (x,r) by A79, QC_TRANS:8 ;

hence S

for x being bound_QC-variable of Al2

for k being Nat

for l being CQC-variable_list of k,Al2

for P being QC-pred_symbol of k,Al2 holds

( S

for p being Element of CQC-WFF Al2 holds S

hence for p being Element of CQC-WFF Al2 ex n being Element of NAT st p is Element of CQC-WFF H

proof

hence
ex Al2 being Al -expanding QC-alphabet ex PSI being Consistent Subset of (CQC-WFF Al2) st
for x being bound_QC-variable of Al2

for p being Element of CQC-WFF Al2 ex y being bound_QC-variable of Al2 st PSI |- ('not' (Ex (x,p))) 'or' (p . (x,y))

end;for p being Element of CQC-WFF Al2 ex y being bound_QC-variable of Al2 st PSI |- ('not' (Ex (x,p))) 'or' (p . (x,y))

proof

hence
PSI is with_examples
by GOEDELCP:def 2; :: thesis: verum
let x be bound_QC-variable of Al2; :: thesis: for p being Element of CQC-WFF Al2 ex y being bound_QC-variable of Al2 st PSI |- ('not' (Ex (x,p))) 'or' (p . (x,y))

let p be Element of CQC-WFF Al2; :: thesis: ex y being bound_QC-variable of Al2 st PSI |- ('not' (Ex (x,p))) 'or' (p . (x,y))

ex n being Element of NAT st

( x is bound_QC-variable of H_{1}(n) & p is Element of CQC-WFF H_{1}(n) )

A89: ( x is bound_QC-variable of H_{1}(n) & p is Element of CQC-WFF H_{1}(n) )
;

A90: FCEx H_{1}(n) = H_{1}(n + 1)
by Th5;

A91: H_{2}(n + 1) = H_{2}(n) \/ (Example_Formulae_of H_{1}(n))
by Def9;

consider x2 being bound_QC-variable of H_{1}(n), p2 being Element of CQC-WFF H_{1}(n) such that

A92: ( x2 = x & p2 = p ) by A89;

Example_Formula_of (p2,x2) in Example_Formulae_of H_{1}(n)
;

then A93: Example_Formula_of (p2,x2) in H_{2}(n + 1)
by A91, XBOOLE_0:def 3;

H_{1}(n) c= H_{1}(n + 1)
by Th6, NAT_1:11;

then reconsider Sn1 = H_{1}(n + 1) as H_{1}(n) -expanding QC-alphabet by QC_TRANS:def 1;

set y2 = Example_of (p2,x2);

reconsider y2 = Example_of (p2,x2) as bound_QC-variable of Sn1 by Th5;

reconsider Al2 = Al2 as Sn1 -expanding QC-alphabet by A2, QC_TRANS:def 1;

y2 is bound_QC-variable of Al2 by TARSKI:def 3, QC_TRANS:4;

then consider y being bound_QC-variable of Al2 such that

A94: y = y2 ;

A95: ( Sn1 -Cast p2 = p & Sn1 -Cast x2 = x ) by A92, QC_TRANS:def 3, QC_TRANS:def 4;

then A96: ( Al2 -Cast (Sn1 -Cast p2) = p & Al2 -Cast (Sn1 -Cast x2) = x ) by QC_TRANS:def 3, QC_TRANS:def 4;

A97: Al2 -Cast (Ex ((Sn1 -Cast x2),(Sn1 -Cast p2))) = Ex (x,p) by A96, Th7;

reconsider p = p as Element of CQC-WFF Al2 ;

reconsider x = x as bound_QC-variable of Al2 ;

A98: (Sn1 -Cast p2) . ((Sn1 -Cast x2),y2) = p . (x,y) by A94, A95, QC_TRANS:17;

A99: Example_Formula_of (p2,x2) = Al2 -Cast (('not' (Ex ((Sn1 -Cast x2),(Sn1 -Cast p2)))) 'or' ((Sn1 -Cast p2) . ((Sn1 -Cast x2),y2))) by A90, QC_TRANS:def 3

.= (Al2 -Cast ('not' (Ex ((Sn1 -Cast x2),(Sn1 -Cast p2))))) 'or' (Al2 -Cast ((Sn1 -Cast p2) . ((Sn1 -Cast x2),y2))) by Th7

.= ('not' (Al2 -Cast (Ex ((Sn1 -Cast x2),(Sn1 -Cast p2))))) 'or' (Al2 -Cast ((Sn1 -Cast p2) . ((Sn1 -Cast x2),y2))) by QC_TRANS:8

.= ('not' (Ex (x,p))) 'or' (p . (x,y)) by A97, A98, QC_TRANS:def 3 ;

set example = ('not' (Ex (x,p))) 'or' (p . (x,y));

reconsider example = ('not' (Ex (x,p))) 'or' (p . (x,y)) as Element of CQC-WFF Al2 ;

reconsider PSI = PSI as Consistent Subset of (CQC-WFF Al2) ;

H_{2}(n + 1) in { H_{2}(m) where m is Element of NAT : verum }
;

then H_{2}(n + 1) c= PSI
by ZFMISC_1:74;

hence ex y being bound_QC-variable of Al2 st PSI |- ('not' (Ex (x,p))) 'or' (p . (x,y)) by A93, A99, GOEDELCP:21; :: thesis: verum

end;let p be Element of CQC-WFF Al2; :: thesis: ex y being bound_QC-variable of Al2 st PSI |- ('not' (Ex (x,p))) 'or' (p . (x,y))

ex n being Element of NAT st

( x is bound_QC-variable of H

proof

then consider n being Element of NAT such that
consider m being Element of NAT such that

A81: p is Element of CQC-WFF H_{1}(m)
by A43;

( x in QC-variables Al2 & QC-variables Al2 c= [:NAT,(QC-symbols Al2):] ) by QC_LANG1:4;

then ( x in [:NAT,(QC-symbols Al2):] & Al2 = [:NAT,(QC-symbols Al2):] ) by QC_LANG1:5;

then ( {x} c= union S & {x} is finite ) by ZFMISC_1:31;

then consider a being set such that

A82: ( a in S & {x} c= a ) by A39, COHSP_1:6, COHSP_1:13;

consider n being Element of NAT such that

A83: a = H_{1}(n)
by A82;

x in bound_QC-variables Al2 ;

then x in [:{4},(QC-symbols Al2):] by QC_LANG1:def 4;

then consider x1, x2 being object such that

A84: ( x1 in {4} & x2 in QC-symbols Al2 & x = [x1,x2] ) by ZFMISC_1:def 2;

A85: x in H_{1}(n)
by A82, A83, ZFMISC_1:31;

end;A81: p is Element of CQC-WFF H

( x in QC-variables Al2 & QC-variables Al2 c= [:NAT,(QC-symbols Al2):] ) by QC_LANG1:4;

then ( x in [:NAT,(QC-symbols Al2):] & Al2 = [:NAT,(QC-symbols Al2):] ) by QC_LANG1:5;

then ( {x} c= union S & {x} is finite ) by ZFMISC_1:31;

then consider a being set such that

A82: ( a in S & {x} c= a ) by A39, COHSP_1:6, COHSP_1:13;

consider n being Element of NAT such that

A83: a = H

x in bound_QC-variables Al2 ;

then x in [:{4},(QC-symbols Al2):] by QC_LANG1:def 4;

then consider x1, x2 being object such that

A84: ( x1 in {4} & x2 in QC-symbols Al2 & x = [x1,x2] ) by ZFMISC_1:def 2;

A85: x in H

per cases
( n <= m or not n <= m )
;

end;

suppose A86:
n <= m
; :: thesis: ex n being Element of NAT st

( x is bound_QC-variable of H_{1}(n) & p is Element of CQC-WFF H_{1}(n) )

( x is bound_QC-variable of H

then reconsider Sm = H_{1}(m) as H_{1}(n) -expanding QC-alphabet by Th6, QC_TRANS:def 1;

H_{1}(n) c= H_{1}(m)
by A86, Th6;

then x in H_{1}(m)
by A85;

then x in [:NAT,(QC-symbols H_{1}(m)):]
by QC_LANG1:5;

then consider x3, x4 being object such that

A87: ( x3 in NAT & x4 in QC-symbols H_{1}(m) & x = [x3,x4] )
by ZFMISC_1:def 2;

x = [x1,x4] by A84, A87, XTUPLE_0:1;

then x in [:{4},(QC-symbols Sm):] by A84, A87, ZFMISC_1:def 2;

then x is bound_QC-variable of Sm by QC_LANG1:def 4;

hence ex n being Element of NAT st

( x is bound_QC-variable of H_{1}(n) & p is Element of CQC-WFF H_{1}(n) )
by A81; :: thesis: verum

end;H

then x in H

then x in [:NAT,(QC-symbols H

then consider x3, x4 being object such that

A87: ( x3 in NAT & x4 in QC-symbols H

x = [x1,x4] by A84, A87, XTUPLE_0:1;

then x in [:{4},(QC-symbols Sm):] by A84, A87, ZFMISC_1:def 2;

then x is bound_QC-variable of Sm by QC_LANG1:def 4;

hence ex n being Element of NAT st

( x is bound_QC-variable of H

suppose
not n <= m
; :: thesis: ex n being Element of NAT st

( x is bound_QC-variable of H_{1}(n) & p is Element of CQC-WFF H_{1}(n) )

( x is bound_QC-variable of H

then reconsider Sn = H_{1}(n) as H_{1}(m) -expanding QC-alphabet by Th6, QC_TRANS:def 1;

x in [:NAT,(QC-symbols H_{1}(n)):]
by A85, QC_LANG1:5;

then consider x3, x4 being object such that

A88: ( x3 in NAT & x4 in QC-symbols H_{1}(n) & x = [x3,x4] )
by ZFMISC_1:def 2;

x = [x1,x4] by A84, A88, XTUPLE_0:1;

then x in [:{4},(QC-symbols Sn):] by A84, A88, ZFMISC_1:def 2;

then ( x is bound_QC-variable of Sn & p is Element of CQC-WFF Sn ) by A81, QC_TRANS:7, QC_LANG1:def 4;

hence ex n being Element of NAT st

( x is bound_QC-variable of H_{1}(n) & p is Element of CQC-WFF H_{1}(n) )
; :: thesis: verum

end;x in [:NAT,(QC-symbols H

then consider x3, x4 being object such that

A88: ( x3 in NAT & x4 in QC-symbols H

x = [x1,x4] by A84, A88, XTUPLE_0:1;

then x in [:{4},(QC-symbols Sn):] by A84, A88, ZFMISC_1:def 2;

then ( x is bound_QC-variable of Sn & p is Element of CQC-WFF Sn ) by A81, QC_TRANS:7, QC_LANG1:def 4;

hence ex n being Element of NAT st

( x is bound_QC-variable of H

A89: ( x is bound_QC-variable of H

A90: FCEx H

A91: H

consider x2 being bound_QC-variable of H

A92: ( x2 = x & p2 = p ) by A89;

Example_Formula_of (p2,x2) in Example_Formulae_of H

then A93: Example_Formula_of (p2,x2) in H

H

then reconsider Sn1 = H

set y2 = Example_of (p2,x2);

reconsider y2 = Example_of (p2,x2) as bound_QC-variable of Sn1 by Th5;

reconsider Al2 = Al2 as Sn1 -expanding QC-alphabet by A2, QC_TRANS:def 1;

y2 is bound_QC-variable of Al2 by TARSKI:def 3, QC_TRANS:4;

then consider y being bound_QC-variable of Al2 such that

A94: y = y2 ;

A95: ( Sn1 -Cast p2 = p & Sn1 -Cast x2 = x ) by A92, QC_TRANS:def 3, QC_TRANS:def 4;

then A96: ( Al2 -Cast (Sn1 -Cast p2) = p & Al2 -Cast (Sn1 -Cast x2) = x ) by QC_TRANS:def 3, QC_TRANS:def 4;

A97: Al2 -Cast (Ex ((Sn1 -Cast x2),(Sn1 -Cast p2))) = Ex (x,p) by A96, Th7;

reconsider p = p as Element of CQC-WFF Al2 ;

reconsider x = x as bound_QC-variable of Al2 ;

A98: (Sn1 -Cast p2) . ((Sn1 -Cast x2),y2) = p . (x,y) by A94, A95, QC_TRANS:17;

A99: Example_Formula_of (p2,x2) = Al2 -Cast (('not' (Ex ((Sn1 -Cast x2),(Sn1 -Cast p2)))) 'or' ((Sn1 -Cast p2) . ((Sn1 -Cast x2),y2))) by A90, QC_TRANS:def 3

.= (Al2 -Cast ('not' (Ex ((Sn1 -Cast x2),(Sn1 -Cast p2))))) 'or' (Al2 -Cast ((Sn1 -Cast p2) . ((Sn1 -Cast x2),y2))) by Th7

.= ('not' (Al2 -Cast (Ex ((Sn1 -Cast x2),(Sn1 -Cast p2))))) 'or' (Al2 -Cast ((Sn1 -Cast p2) . ((Sn1 -Cast x2),y2))) by QC_TRANS:8

.= ('not' (Ex (x,p))) 'or' (p . (x,y)) by A97, A98, QC_TRANS:def 3 ;

set example = ('not' (Ex (x,p))) 'or' (p . (x,y));

reconsider example = ('not' (Ex (x,p))) 'or' (p . (x,y)) as Element of CQC-WFF Al2 ;

reconsider PSI = PSI as Consistent Subset of (CQC-WFF Al2) ;

H

then H

hence ex y being bound_QC-variable of Al2 st PSI |- ('not' (Ex (x,p))) 'or' (p . (x,y)) by A93, A99, GOEDELCP:21; :: thesis: verum

( PHI c= PSI & PSI is with_examples ) by A1; :: thesis: verum