let p be boolean number ; :: thesis: p = p * p
( p = FALSE or p = TRUE ) by Def3;
hence p = p * p ; :: thesis: verum