theorem Th16: :: RAMSEY_1:16

for n, m being Nat st m >= 2 & n >= 2 holds
ex r being Nat st
( r <= ((m + n) -' 2) choose (m -' 1) & r >= 2 & ( for X being finite set
for F being Function of (the_subsets_of_card (2,X)),(Seg 2) st card X >= r holds
ex S being Subset of X st
( ( card S >= m & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= n & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) ) )