let p, q be boolean object ; :: thesis: (p '&' q) => p = TRUE
( p = TRUE or p = FALSE ) by XBOOLEAN:def 3;
hence (p '&' q) => p = TRUE ; :: thesis: verum