let X be Subset of CQC-WFF ; :: thesis: for A being non empty set st not X is Consistent holds
for J being interpretation of A
for v being Element of Valuations_in A holds not J,v |= X
let A be non empty set ; :: thesis: ( not X is Consistent implies for J being interpretation of A
for v being Element of Valuations_in A holds not J,v |= X )
reconsider p = 'not' VERUM as Element of CQC-WFF ;
assume not X is Consistent ; :: thesis: for J being interpretation of A
for v being Element of Valuations_in A holds not J,v |= X
then X |- 'not' VERUM by Th6;
then consider f being FinSequence of CQC-WFF such that
A1: rng f c= X and
A2: |- f ^ <*('not' VERUM )*> by Def2;
let J be interpretation of A; :: thesis: for v being Element of Valuations_in A holds not J,v |= X
let v be Element of Valuations_in 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

assume J,v |= X ; :: thesis: contradiction
then J,v |= 'not' VERUM by A4, CALCUL_1:def 12;
then not J,v |= VERUM by VALUAT_1:28;
hence contradiction by VALUAT_1:44; :: thesis: verum

end;

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