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