:: deftheorem Def15 defines ALL MARGREL1:def 15 :
for X being set holds
( ( not FALSE in X implies ALL X = TRUE ) & ( FALSE in X implies ALL X = FALSE ) );