theorem Th15: :: WSIERP_1:15

for a being Nat st a divides 1 holds
a = 1