theorem :: MARGREL1:17

for X being set holds
( ( not FALSE in X implies ALL X = TRUE ) & ( ALL X = TRUE implies not FALSE in X ) & ( FALSE in X implies ALL X = FALSE ) & ( ALL X = FALSE implies FALSE in X ) ) by Def15;