theorem Th38: :: CATALAN2:38

for n being Nat st n > 0 holds
Domin_0 ((2 * n),n) = { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((2 * n),n) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) }