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