0c = 0 ;
hence ( ( m <= k implies 1 is Element of COMPLEX ) & ( not m <= k implies 0 is Element of COMPLEX ) & ( for b₁ being Element of COMPLEX holds verum ) ) by COMPLEX1:def 4; :: thesis: verum