thus Parity a = 1 by NAT_2:def 1
.= parity a by NAT_2:def 1 ; :: thesis: verum