let f be Function of NAT ,(bool CQC-WFF ); :: thesis: ( ( for n, m being Element of 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 Element of 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

A2: for n being Element of NAT st n in dom f holds
f . n is Consistent

proof

let n be Element of 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 such that
A4: ( Z c= union (rng f) & Z is finite ) and
A5: not Z is Consistent by Th7;
for n, m being Element of NAT st m in dom f & n in dom f & n < m holds
f . n c= f . m by A1;
then consider k being Element of NAT such that
A6: Z c= f . k by A4, Th3;
reconsider Y = f . k as Subset of CQC-WFF ;
consider p being Element of CQC-WFF such that
A7: Z |- p and
A8: Z |- 'not' p by A5, Def3;
consider f1 being FinSequence of CQC-WFF such that
A9: rng f1 c= Z and
A10: |- f1 ^ <*p*> by A7, Def2;
consider f2 being FinSequence of CQC-WFF such that
A11: rng f2 c= Z and
A12: |- f2 ^ <*('not' p)*> by A8, Def2;
rng (f1 ^ f2) = (rng f1) \/ (rng f2) by FINSEQ_1:44;
then rng (f1 ^ f2) c= Z by A9, A11, XBOOLE_1:8;
then A13: rng (f1 ^ f2) c= Y by A6, XBOOLE_1:1;
|- (f1 ^ f2) ^ <*('not' p)*> by A12, CALCUL_2:20;
then A14: Y |- 'not' p by A13, Def2;
|- (f1 ^ f2) ^ <*p*> by A10, Th5;
then Y |- p by A13, Def2;
then A15: not Y is Consistent by A14, Def3;
k in NAT ;
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