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