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 by A1, Def11;
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