let p, q, r be boolean object ; :: thesis: ((p '&' q) 'or' (q '&' r)) 'or' (r '&' p) = ((p 'or' q) '&' (q 'or' r)) '&' (r 'or' p)
A1: ( q = FALSE or q = TRUE ) by Def3;
( p = FALSE or p = TRUE ) by Def3;
hence ((p '&' q) 'or' (q '&' r)) 'or' (r '&' p) = ((p 'or' q) '&' (q 'or' r)) '&' (r 'or' p) by A1; :: thesis: verum