hereby :: thesis: ( x in BOOLEAN implies x is boolean )

assume x is boolean ; :: thesis: x in BOOLEAN
then ( x = FALSE or x = TRUE ) by XBOOLEAN:def 3;
hence x in BOOLEAN ; :: thesis: verum

end;

assume x in BOOLEAN ; :: thesis: x is boolean
hence ( x = FALSE or x = TRUE ) by TARSKI:def 2; :: according to XBOOLEAN:def 3 :: thesis: verum