set Phi = <*l*> ^ phi;
<*l*> ^ phi = (<*l*> ^ phi) null {}
.= (<*l*> ^ phi) ^ {} ;
then phi = head (<*l*> ^ phi) by Th23;
hence (head (<*l*> ^ phi)) \+\ phi is empty ; :: thesis: verum