( phi0 = [phi0,{}] `1 & SubWffsOf phi0 = [phi0,{}] ) by Def34;
hence head phi0 = phi0 null ; :: thesis: verum