take 0 .--> 0 ; :: thesis: ( not 0 .--> 0 is empty & 0 .--> 0 is trivial & 0 .--> 0 is NAT -defined & 0 .--> 0 is finite )
thus ( not 0 .--> 0 is empty & 0 .--> 0 is trivial & 0 .--> 0 is NAT -defined & 0 .--> 0 is finite ) ; :: thesis: verum