card p = card p ;
hence len p is Element of NAT ; :: thesis: verum