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