theorem :: XBOOLEAN:108

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