let Al be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF Al) holds
( X |- 'not' (VERUM Al) iff X is Inconsistent )
let X be Subset of (CQC-WFF Al); :: thesis: ( X |- 'not' (VERUM Al) iff X is Inconsistent )
thus ( X |- 'not' (VERUM Al) implies X is Inconsistent ) :: thesis: ( X is Inconsistent implies X |- 'not' (VERUM Al) )

proof

assume A1: X |- 'not' (VERUM Al) ; :: thesis: X is Inconsistent
X |- VERUM Al by Th23;
hence X is Inconsistent by A1, HENMODEL:def 2; :: thesis: verum

end;

thus ( X is Inconsistent implies X |- 'not' (VERUM Al) ) by HENMODEL:6; :: thesis: verum