( 1 is trivial & 1 <> 0 ) ;
hence ex b₁ being Nat st
( b₁ is trivial & not b₁ is zero ) ; :: thesis: verum