:: deftheorem Def7 defines conditional HILBERT2:def 7 :
for p being Element of HP-WFF holds
( p is conditional iff ex r, s being Element of HP-WFF st p = r => s );