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