for V being RealLinearSpace
for A being Subset of V st not Int A is empty holds
A is finite