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