3 * 3 = 9 ;
then 3 divides 9 ;
then not 9 is prime ;
hence ex b₁ being Nat st
( b₁ is Proth & not b₁ is prime ) by Lm7; :: thesis: verum