take Theorems P ; :: thesis: Theorems P is P -closed
thus Theorems P is P -closed ; :: thesis: verum