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