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