([phi0,{}] `1) \+\ phi0 = {} ;
then ( phi0 = [phi0,{}] `1 & SubWffsOf phi0 = [phi0,{}] ) by DefSub1, FOMODEL0:29;
hence head phi0 = phi0 null ; :: thesis: verum