:: deftheorem defines '&' MARGREL1:def 14 :
for v, w being boolean object holds
( ( v = TRUE & w = TRUE implies v '&' w = TRUE ) & ( ( not v = TRUE or not w = TRUE ) implies v '&' w = FALSE ) );