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

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

hence
g is Consistent
; :: thesis: verumassume
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;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