theorem :: XBOOLEAN:132

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