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 object such that

A1: x in Int A ;

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

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 object such that

A1: x in Int A ;

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