let Al be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF Al)
for g being FinSequence of CQC-WFF Al st X is Consistent & rng g c= X holds
g is Consistent
let X be Subset of (CQC-WFF Al); :: thesis: for g being FinSequence of CQC-WFF Al st X is Consistent & rng g c= X holds
g is Consistent
let g be FinSequence of CQC-WFF Al; :: thesis: ( X is Consistent & rng g c= X implies g is Consistent )
assume that
A1: X is Consistent and
A2: rng g c= X ; :: thesis: g is Consistent
now :: thesis: not g is Inconsistent
assume g is Inconsistent ; :: thesis: contradiction
then consider p being Element of CQC-WFF Al such that
A3: ( |- g ^ <*p*> & |- g ^ <*('not' p)*> ) ;
( X |- p & X |- 'not' p ) by A2, A3;
hence contradiction by A1; :: thesis: verum
end;
hence g is Consistent ; :: thesis: verum