theorem :: XBOOLEAN:104

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