theorem :: XBOOLEAN:112

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