let V be RealLinearSpace; :: thesis: for A being Subset of V st not Int A is empty holds
A is finite
let A be Subset of V; :: thesis: ( not Int A is empty implies A is finite )
assume not Int A is empty ; :: thesis: A is finite
then consider x being set such that
A1: x in Int A by XBOOLE_0:def 1;
consider L being Linear_Combination of A such that
A2: ( L is convex & x = Sum L ) by A1, Th10;
Carrier L = A by A1, A2, Th11;
hence A is finite ; :: thesis: verum