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 A1, CALCUL_1:5;
then p is_formal_provable_from X by A2, A3, CALCUL_1:def 10;
then A4: X |= p by CALCUL_1:32;

now :: thesis: not J,v |= X

assume J,v |= X ; :: thesis: contradiction
then J,v |= 'not' (VERUM Al) by A4, CALCUL_1:def 12;
then not J,v |= VERUM Al by VALUAT_1:17;
hence contradiction by VALUAT_1:32; :: thesis: verum

end;

hence not J,v |= X ; :: thesis: verum