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;

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

hence
not J,v |= X
; :: thesis: verumassume
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;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