A2: for n being Nat st n in dom f holds
f . n is Consistent 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