theorem Th6: :: HILB10_1:3
for a being non trivial Nat holds
( Px (a,0) = 1 & Py (a,0) = 0 )