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