let T be Subset of HP-WFF; :: thesis: ( T is Hilbert_theory iff CnPos T = T )

hereby :: thesis: ( CnPos T = T implies T is Hilbert_theory )

assume A1: T is Hilbert_theory ; :: thesis: CnPos T = T
A2: CnPos T c= T

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in CnPos T or a in T )
assume a in CnPos T ; :: thesis: a in T
hence a in T by A1, Def11; :: thesis: verum

end;

T c= CnPos T by Th9;
hence CnPos T = T by A2, XBOOLE_0:def 10; :: thesis: verum

end;

thus ( CnPos T = T implies T is Hilbert_theory ) ; :: thesis: verum