theorem Th2: :: SIMPLEX1:2

for X being set
for Y being non empty finite set st card X = (card Y) + 1 holds
for f being Function of X,Y st f is onto holds
ex y being set st
( y in Y & card (f " {y}) = 2 & ( for x being set st x in Y & x <> y holds
card (f " {x}) = 1 ) )