let X be Subset of CQC-WFF ; :: thesis: ( X |- 'not' VERUM iff not X is Consistent )
thus ( X |- 'not' VERUM implies not X is Consistent ) :: thesis: ( not X is Consistent implies X |- 'not' VERUM )

proof

assume A1: X |- 'not' VERUM ; :: thesis: not X is Consistent
X |- VERUM by Th23;
hence not X is Consistent by A1, HENMODEL:def 3; :: thesis: verum

end;

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