take NAT --> the plain _Graph ; :: thesis: NAT --> the plain _Graph is plain
thus NAT --> the plain _Graph is plain ; :: thesis: verum