let X be Subset of CQC-WFF ; :: thesis: for g being FinSequence of CQC-WFF st X is Consistent & rng g c= X holds
g is Consistent
let g be FinSequence of CQC-WFF ; :: thesis: ( X is Consistent & rng g c= X implies g is Consistent )
assume A1: ( X is Consistent & rng g c= X ) ; :: thesis: g is Consistent

now

assume not g is Consistent ; :: thesis: contradiction
then consider p being Element of CQC-WFF such that
A2: ( |- g ^ <*p*> & |- g ^ <*('not' p)*> ) by Def4;
( X |- p & X |- 'not' p ) by A1, A2, Def2;
hence contradiction by A1, Def3; :: thesis: verum

end;

hence g is Consistent ; :: thesis: verum