1. L divides 1. L ;
hence ex b₁ being Element of L st b₁ is unital by GCD_1:def 2; :: thesis: verum