take B ; :: thesis: B is B -headed
thus B is B -headed by Th15; :: thesis: verum