:: deftheorem Def5 defines PL-closed PL_AXIOM:def 2 :
for D being set holds
( D is PL-closed iff ( D c= NAT * & D is with_FALSUM & D is with_implication & D is with_propositional_variables ) );