take 0 .--> 0 ; :: thesis: ( 0 .--> 0 is 1 -element & 0 .--> 0 is NAT -defined & 0 .--> 0 is finite )
thus ( 0 .--> 0 is 1 -element & 0 .--> 0 is NAT -defined & 0 .--> 0 is finite ) ; :: thesis: verum