theorem :: MARGREL1:12

for v, w being boolean object holds
( ( v '&' w = TRUE implies ( v = TRUE & w = TRUE ) ) & ( v = TRUE & w = TRUE implies v '&' w = TRUE ) & ( not v '&' w = FALSE or v = FALSE or w = FALSE ) & ( ( v = FALSE or w = FALSE ) implies v '&' w = FALSE ) ) by XBOOLEAN:101, XBOOLEAN:140;