let Al be QC-alphabet ; :: thesis: for f being sequence of (bool (CQC-WFF Al)) st ( 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 ) ) holds

union (rng f) is Consistent

let f be sequence of (bool (CQC-WFF Al)); :: thesis: ( ( 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 ) ) implies union (rng f) is Consistent )

assume A1: 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 ) ; :: thesis: union (rng f) is Consistent

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

union (rng f) is Consistent

let f be sequence of (bool (CQC-WFF Al)); :: thesis: ( ( 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 ) ) implies union (rng f) is Consistent )

assume A1: 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 ) ; :: thesis: union (rng f) is Consistent

now :: thesis: union (rng f) is Consistent

hence
union (rng f) is Consistent
; :: thesis: verumA2:
for n being Nat st n in dom f holds

f . n is Consistent

then consider Z being Subset of (CQC-WFF Al) such that

A4: ( Z c= union (rng f) & Z is finite ) and

A5: Z is Inconsistent by Th7;

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

f . n c= f . m by A1;

then consider k being Nat such that

A6: Z c= f . k by A4, Th3;

reconsider Y = f . k as Subset of (CQC-WFF Al) ;

consider p being Element of CQC-WFF Al such that

A7: Z |- p and

A8: Z |- 'not' p by A5;

consider f1 being FinSequence of CQC-WFF Al such that

A9: rng f1 c= Z and

A10: |- f1 ^ <*p*> by A7;

consider f2 being FinSequence of CQC-WFF Al such that

A11: rng f2 c= Z and

A12: |- f2 ^ <*('not' p)*> by A8;

rng (f1 ^ f2) = (rng f1) \/ (rng f2) by FINSEQ_1:31;

then rng (f1 ^ f2) c= Z by A9, A11, XBOOLE_1:8;

then A13: rng (f1 ^ f2) c= Y by A6;

|- (f1 ^ f2) ^ <*('not' p)*> by A12, CALCUL_2:20;

then A14: Y |- 'not' p by A13;

|- (f1 ^ f2) ^ <*p*> by A10, Th5;

then Y |- p by A13;

then A15: not Y is Consistent by A14;

k in NAT by ORDINAL1:def 12;

then k in dom f by FUNCT_2:def 1;

hence contradiction by A15, A2; :: thesis: verum

end;f . n is Consistent

proof

assume
not union (rng f) is Consistent
; :: thesis: contradiction
let n be Nat; :: thesis: ( n in dom f implies f . n is Consistent )

assume A3: n in dom f ; :: thesis: f . n is Consistent

n + 1 in NAT ;

then ( n < n + 1 & n + 1 in dom f ) by FUNCT_2:def 1, NAT_1:13;

hence f . n is Consistent by A1, A3; :: thesis: verum

end;assume A3: n in dom f ; :: thesis: f . n is Consistent

n + 1 in NAT ;

then ( n < n + 1 & n + 1 in dom f ) by FUNCT_2:def 1, NAT_1:13;

hence f . n is Consistent by A1, A3; :: thesis: verum

then consider Z being Subset of (CQC-WFF Al) such that

A4: ( Z c= union (rng f) & Z is finite ) and

A5: Z is Inconsistent by Th7;

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

f . n c= f . m by A1;

then consider k being Nat such that

A6: Z c= f . k by A4, Th3;

reconsider Y = f . k as Subset of (CQC-WFF Al) ;

consider p being Element of CQC-WFF Al such that

A7: Z |- p and

A8: Z |- 'not' p by A5;

consider f1 being FinSequence of CQC-WFF Al such that

A9: rng f1 c= Z and

A10: |- f1 ^ <*p*> by A7;

consider f2 being FinSequence of CQC-WFF Al such that

A11: rng f2 c= Z and

A12: |- f2 ^ <*('not' p)*> by A8;

rng (f1 ^ f2) = (rng f1) \/ (rng f2) by FINSEQ_1:31;

then rng (f1 ^ f2) c= Z by A9, A11, XBOOLE_1:8;

then A13: rng (f1 ^ f2) c= Y by A6;

|- (f1 ^ f2) ^ <*('not' p)*> by A12, CALCUL_2:20;

then A14: Y |- 'not' p by A13;

|- (f1 ^ f2) ^ <*p*> by A10, Th5;

then Y |- p by A13;

then A15: not Y is Consistent by A14;

k in NAT by ORDINAL1:def 12;

then k in dom f by FUNCT_2:def 1;

hence contradiction by A15, A2; :: thesis: verum