theorem Th5: :: MATROID0:5

for A, B being finite set st card A < card B holds
ex x being set st x in B \ A