let Al be QC-alphabet ; 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); 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 ; ( 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
; 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; for v being Element of Valuations_in (Al,A) holds not J,v |= X
let v be Element of Valuations_in (Al,A); 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;
hence
not J,v |= X
; verum