:: deftheorem Def6 defines conjunctive HILBERT2:def 6 :
for p being Element of HP-WFF holds
( p is conjunctive iff ex r, s being Element of HP-WFF st p = r '&' s );