let p, q be boolean object ; :: thesis: ('not' (p 'or' q)) <=> (('not' p) '&' ('not' q)) = TRUE
A1: ( p = TRUE or p = FALSE ) by XBOOLEAN:def 3;
( q = TRUE or q = FALSE ) by XBOOLEAN:def 3;
hence ('not' (p 'or' q)) <=> (('not' p) '&' ('not' q)) = TRUE by A1; :: thesis: verum