let X be Subset of CQC-WFF ; :: thesis: ( not X is Consistent iff for p being Element of CQC-WFF holds X |- p )
thus ( not X is Consistent implies for p being Element of CQC-WFF holds X |- p ) :: thesis: ( ( for p being Element of CQC-WFF holds X |- p ) implies not X is Consistent )

proof

assume not X is Consistent ; :: thesis: for p being Element of CQC-WFF holds X |- p
then consider q being Element of CQC-WFF such that
A1: ( X |- q & X |- 'not' q ) by Def3;
let p be Element of CQC-WFF ; :: thesis: X |- p
consider f1 being FinSequence of CQC-WFF such that
A2: ( rng f1 c= X & |- f1 ^ <*q*> ) by A1, Def2;
consider f2 being FinSequence of CQC-WFF such that
A3: ( rng f2 c= X & |- f2 ^ <*('not' q)*> ) by A1, Def2;
A4: ( |- (f1 ^ f2) ^ <*q*> & |- (f1 ^ f2) ^ <*('not' q)*> ) by A2, A3, Th5, CALCUL_2:20;
take f3 = f1 ^ f2; :: according to HENMODEL:def 2 :: thesis: ( rng f3 c= X & |- f3 ^ <*p*> )
rng f3 = (rng f1) \/ (rng f2) by FINSEQ_1:44;
hence ( rng f3 c= X & |- f3 ^ <*p*> ) by A2, A3, A4, CALCUL_2:25, XBOOLE_1:8; :: thesis: verum

end;

assume for p being Element of CQC-WFF holds X |- p ; :: thesis: not X is Consistent
then ( X |- VERUM & X |- 'not' VERUM ) ;
hence not X is Consistent by Def3; :: thesis: verum