for x being Element of L holds
( 1. L <> (0. L) * x or 1. L <> x * (0. L) ) ;
hence not for b₁ being Element of L holds b₁ is unital by GCD_1:def 2; :: thesis: verum