:: deftheorem Def5 defines HP-closed HILBERT1:def 5 :
for D being set holds
( D is HP-closed iff ( D c= NAT * & D is with_VERUM & D is with_implication & D is with_conjunction & D is with_propositional_variables ) );