let Al be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF Al)
for A being non empty set st X is Inconsistent holds
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) holds not J,v |= X

let X be Subset of (CQC-WFF Al); :: thesis: for A being non empty set st X is Inconsistent holds
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) holds not J,v |= X

let A be non empty set ; :: thesis: ( X is Inconsistent implies for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) holds not J,v |= X )

reconsider p = 'not' (VERUM Al) as Element of CQC-WFF Al ;
assume not X is Consistent ; :: thesis: for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) holds not J,v |= X

then X |- 'not' (VERUM Al) by Th6;
then consider f being FinSequence of CQC-WFF Al such that
A1: rng f c= X and
A2: |- f ^ <*('not' (VERUM Al))*> ;
let J be interpretation of Al,A; :: thesis: for v being Element of Valuations_in (Al,A) holds not J,v |= X
let v be Element of Valuations_in (Al,A); :: thesis: not J,v |= X
A3: Suc (f ^ <*p*>) = p by CALCUL_1:5;
rng (Ant (f ^ <*p*>)) c= X by ;
then p is_formal_provable_from X by ;
then A4: X |= p by CALCUL_1:32;
now :: thesis: not J,v |= Xend;
hence not J,v |= X ; :: thesis: verum