theorem th1: :: PL_AXIOM:2

for p, q being boolean object holds (p '&' q) => p = TRUE