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

assume not union (rng f) is Consistent ; :: thesis: contradiction
then consider Z being Subset of CQC-WFF such that
A2: ( Z c= union (rng f) & Z is finite & not Z is Consistent ) by Th7;
consider p being Element of CQC-WFF such that
A3: ( Z |- p & Z |- 'not' p ) by A2, Def3;
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
A4: Z c= f . k by A2, Th3;
reconsider Y = f . k as Subset of CQC-WFF ;
consider f1 being FinSequence of CQC-WFF such that
A5: ( rng f1 c= Z & |- f1 ^ <*p*> ) by A3, Def2;
consider f2 being FinSequence of CQC-WFF such that
A6: ( rng f2 c= Z & |- f2 ^ <*('not' p)*> ) by A3, Def2;
A7: ( |- (f1 ^ f2) ^ <*p*> & |- (f1 ^ f2) ^ <*('not' p)*> ) by A5, A6, Th5, CALCUL_2:20;
rng (f1 ^ f2) = (rng f1) \/ (rng f2) by FINSEQ_1:44;
then rng (f1 ^ f2) c= Z by A5, A6, XBOOLE_1:8;
then rng (f1 ^ f2) c= Y by A4, XBOOLE_1:1;
then ( Y |- p & Y |- 'not' p ) by A7, Def2;
then A8: not Y is Consistent by Def3;
A9: 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 A10: 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, A10; :: thesis: verum

end;

k in NAT ;
then k in dom f by FUNCT_2:def 1;
hence contradiction by A8, A9; :: thesis: verum

end;

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