:: deftheorem Def4 defines Castboolean MODELC_1:def 4 :
for a being set holds
( ( a is boolean implies Castboolean a = a ) & ( not a is boolean implies Castboolean a = FALSE ) );