for x being set st x is boolean holds
( x = 1 iff x <> 0 ) by XBOOLEAN:def 3;