:: deftheorem defines head FOMODEL2:def 36 :
for S being Language
for phi being wff string of S holds head phi = (SubWffsOf phi) `1 ;