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

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

A2: for n being Nat st n in dom f holds
f . n is Consistent

proof

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

hence union (rng f) is Consistent ; :: thesis: verum