let x be number ; :: thesis: ( x is boolean implies x is natural )
assume ( x = FALSE or x = TRUE ) ; :: according to XBOOLEAN:def 3 :: thesis: x is natural
hence x is natural ; :: thesis: verum