let p, q, r be boolean object ; :: thesis: (p 'or' (q '&' r)) <=> ((p 'or' q) '&' (p 'or' 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 'or' (q '&' r)) <=> ((p 'or' q) '&' (p 'or' r)) = TRUE by A1, A2; :: thesis: verum