theorem :: BINARI_4:17

for x being boolean object holds TRUE 'or' x = TRUE ;