for p, q being Element of PL-WFF holds (p '&' q) => p is tautology