theorem Th3: :: TOPALG_3:3

for X, a, b being set
for f being Function of X,{a,b} holds X = (f " {a}) \/ (f " {b})