theorem Th16: :: CARDFIL4:17

for A being finite Subset of [:NAT,NAT:] ex m, n being Nat st A c= [:(Segm m),(Segm n):]